contractibleSpace_iff — Mathlib

English

Homotopy equivalences preserve contractibility: X contractible iff Y contractible whenever X ≃ₕ Y.

Русский

Гомотопическая эквивалентность сохраняет контрактность: X контрактно тогда и только тогда, когда Y контрактно, если X ≃ₕ Y.

LaTeX

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

Lean4

protected theorem contractibleSpace_iff (e : X ≃ₕ Y) : ContractibleSpace X ↔ ContractibleSpace Y :=
  ⟨fun _ => e.symm.contractibleSpace, fun _ => e.contractibleSpace⟩

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