withTopCongr_refl — Mathlib

English

The lifting of the identity equivalence is the identity equivalence on WithTop.

Русский

Переносимость тождественной биекции через WithTop равна тождественной биекции на WithTop.

LaTeX

$$$\text{withTopCongr}(\mathrm{Equiv.refl}(\alpha)) = \mathrm{Equiv.refl}(\mathrm{WithTop}(\alpha))$$$

Lean4

@[simp]
theorem withTopCongr_refl : withTopCongr (Equiv.refl α) = Equiv.refl _ :=
  Equiv.ext <| congr_fun WithBot.map_id

Похожие утверждения