contractibleSpace_iff — Mathlib

English

If X and Y are homeomorphic, then X is contractible if and only if Y is contractible.

Русский

Если X гомеоморфен Y, то X конрактно тогда и только тогда, когда Y конрактно.

LaTeX

$$$(e:X\simeq_t Y)\;\Rightarrow\; (\operatorname{ContractibleSpace}(X)\iff \operatorname{ContractibleSpace}(Y)).$$$

Lean4

protected theorem contractibleSpace_iff (e : X ≃ₜ Y) : ContractibleSpace X ↔ ContractibleSpace Y :=
  e.toHomotopyEquiv.contractibleSpace_iff

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