contractibleSpace — Mathlib

English

If Y is contractible, then X is contractible whenever X is homotopy equivalent to Y.

Русский

Если Y контрактно, то X контрактно, когда X гомотопически эквивалентен Y.

LaTeX

$$$ \\forall e:\\,X \\simeq_h Y,\\; ContractibleSpace Y \\to ContractibleSpace X$$$

Lean4

protected theorem contractibleSpace [ContractibleSpace Y] (e : X ≃ₕ Y) : ContractibleSpace X :=
  ⟨(ContractibleSpace.hequiv_unit Y).map e.trans⟩

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