contractible_iff_id_nullhomotopic

English

ContractibleSpace Y is equivalent to id_Y being nullhomotopic.

Русский

Контрактность Y эквивалентна тому, что id_Y является нулевой гомотопией.

LaTeX

$$$ ContractibleSpace Y \\iff (ContinuousMap.id Y).Nullhomotopic$$$

Lean4

theorem contractible_iff_id_nullhomotopic (Y : Type*) [TopologicalSpace Y] :
    ContractibleSpace Y ↔ (ContinuousMap.id Y).Nullhomotopic :=
  by
  constructor
  · intro
    apply id_nullhomotopic
  rintro ⟨p, h⟩
  refine
    {
      hequiv_unit' :=
        ⟨{  toFun := ContinuousMap.const _ ()
            invFun := ContinuousMap.const _ p
            left_inv := ?_
            right_inv := ?_ }⟩ }
  · exact h.symm
  · convert Homotopic.refl (ContinuousMap.id Unit)

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