refl — Mathlib

English

Any topological space is homotopy equivalent to itself; the refl homotopy equivalence is provided by the identity homeomorphism.

Русский

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

LaTeX

$$$X\simeq_h X$$$

Lean4

/-- Any topological space is homotopy equivalent to itself.
-/
@[simps!]
def refl (X : Type u) [TopologicalSpace X] : X ≃ₕ X :=
  (Homeomorph.refl X).toHomotopyEquiv

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