homotopyToZeroOfId — Mathlib

English

The mapping cone of the identity is contractible; there exists a homotopy to zero.

Русский

Отображающий конус тождественного отображения трактируем как контрактный; существует гомотопия к нулю.

LaTeX

$$$Homotopy(\\mathrm{id}_{K}, 0)\\text{ on mappingCone}(\\mathrm{id}_K)$$$

Lean4

/-- The mapping cone of the identity is contractible. -/
noncomputable def homotopyToZeroOfId : Homotopy (𝟙 (mappingCone (𝟙 K))) 0 :=
  descHomotopy (𝟙 K) _ _ 0 (inl _) (by simp) (by simp)

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