hequiv_unit — Mathlib

English

If X is contractible, there exists a homotopy equivalence between X and the unit type Unit.

Русский

Если X контрактно эквивалентна единичному множеству, существует гомотопическая эквивалентность между X и Unit.

LaTeX

$$$ \\exists e:\\,X \\simeq_h Unit$$$

Lean4

theorem hequiv_unit (X : Type*) [TopologicalSpace X] [ContractibleSpace X] : Nonempty (X ≃ₕ Unit) :=
  ContractibleSpace.hequiv_unit'

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