hequiv — Mathlib

English

If X and Y are contractible spaces, then there exists a homotopy equivalence X ≃ₕ Y.

Русский

Если X и Y конрактны, существует гомотопическая эквивалентность X ≃ₕ Y.

LaTeX

$$If $X$ and $Y$ are contractible, then $X \simeq_h Y$; i.e. Nonempty $(X \simeq_h Y)$.$$

Lean4

theorem hequiv [ContractibleSpace X] [ContractibleSpace Y] : Nonempty (X ≃ₕ Y) :=
  by
  rcases ContractibleSpace.hequiv_unit' (X := X) with ⟨h⟩
  rcases ContractibleSpace.hequiv_unit' (X := Y) with ⟨h'⟩
  exact ⟨h.trans h'.symm⟩

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