refl_toHomotopyEquiv — Mathlib

English

The identity homeomorphism refl X corresponds to the identity homotopy equivalence on X.

Русский

тождественный гомеоморфизм refl X соответствует тождественной гомотопической эквивалентности на X.

LaTeX

$$$(Homeomorph.refl X).toHomotopyEquiv = HomotopyEquiv.refl X$$$

Lean4

@[simp]
theorem refl_toHomotopyEquiv (X : Type u) [TopologicalSpace X] :
    (Homeomorph.refl X).toHomotopyEquiv = HomotopyEquiv.refl X :=
  rfl

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