ofContractible — Mathlib

English

If a space Y is contractible, then it is simply connected.

Русский

Если пространство Y контрактируемо, то оно просто связное.

LaTeX

$$$ContractibleSpace Y \Rightarrow SimplyConnectedSpace Y$$$

Lean4

instance (priority := 100) ofContractible (Y : Type u) [TopologicalSpace Y] [ContractibleSpace Y] :
    SimplyConnectedSpace Y where
  equiv_unit :=
    let H : TopCat.of Y ≃ₕ TopCat.of PUnit.{u + 1} := (ContractibleSpace.hequiv Y PUnit.{u + 1}).some
    ⟨(FundamentalGroupoidFunctor.equivOfHomotopyEquiv H).trans FundamentalGroupoid.punitEquivDiscretePUnit⟩

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