id_nullhomotopic — Mathlib

English

The identity map id_X is nullhomotopic when X is contractible.

Русский

Идентичное отображение id_X является нулевой гомотопией, когда X контрактно.

LaTeX

$$$ (ContractibleSpace X) \\to (ContinuousMap.id X).Nullhomotopic$$$

Lean4

theorem id_nullhomotopic (X : Type*) [TopologicalSpace X] [ContractibleSpace X] : (ContinuousMap.id X).Nullhomotopic :=
  by
  obtain ⟨hv⟩ := ContractibleSpace.hequiv_unit X
  use hv.invFun ()
  convert hv.left_inv.symm

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