toHomotopyEquiv — Mathlib

English

Any homeomorphism between spaces induces a homotopy equivalence between them.

Русский

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

LaTeX

$$$\text{toHomotopyEquiv}: X\simeq_t Y \Rightarrow X\simeq_h Y$$$

Lean4

/-- Any homeomorphism is a homotopy equivalence.
-/
def toHomotopyEquiv (h : X ≃ₜ Y) : X ≃ₕ Y where
  toFun := h
  invFun := h.symm
  left_inv := by rw [symm_comp_toContinuousMap]
  right_inv := by rw [toContinuousMap_comp_symm]

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