contractibleSpace — Mathlib

English

Let X and Y be topological spaces with a homeomorphism e: X ≃ₜ Y to a contractible Y. Then X is contractible.

Русский

Пусть X и Y — топологические пространства, существует гомеоморфизм e: X ≃ₜ Y, и Y конрактно. Тогда X конрактно.

LaTeX

$$$\operatorname{ContractibleSpace}(X)\;\text{whenever}\; e:X\simeq_t Y\text{ and } \operatorname{ContractibleSpace}(Y).$$$

Lean4

protected theorem contractibleSpace [ContractibleSpace Y] (e : X ≃ₜ Y) : ContractibleSpace X :=
  e.toHomotopyEquiv.contractibleSpace

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