class SemilocallySimplyConnectedSpace (B : Type u) [TopologicalSpace B] : Prop

Definition 3.8.1: a topological space is semilocally simply connected if every point has an open neighborhood whose inclusion into the ambient space induces the trivial map on the based fundamental group.

• trivial_fundamentalGroup_map (b : B) : ∃ (U : TopologicalSpace.OpenNhdsOf b), FundamentalGroup.map { toFun := Subtype.val, continuous_toFun := ⋯ } ⟨b, ⋯⟩ = 1

  Each point admits an open neighborhood whose inclusion into the ambient space induces the trivial homomorphism on the based fundamental group.

theorem ContinuousMap.Nullhomotopic.fundamentalGroup_map_eq_one {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} (hf : f.Nullhomotopic) (x : X) : FundamentalGroup.map f x = 1

A null-homotopic map induces the trivial morphism on based fundamental groups.

theorem LocallyContractibleSpace.semilocallySimplyConnectedSpace {B : Type u} [TopologicalSpace B] (hB : LocallyContractibleSpace B) : SemilocallySimplyConnectedSpace B

Locally contractible spaces are semilocally simply connected.

instance instSemilocallySimplyConnectedSpaceOfStronglyLocallyContractibleSpace {B : Type u} [TopologicalSpace B] [StronglyLocallyContractibleSpace B] : SemilocallySimplyConnectedSpace B

Strongly locally contractible spaces are semilocally simply connected.

instance instSemilocallySimplyConnectedSpaceOfSimplyConnectedSpace {B : Type u} [TopologicalSpace B] [SimplyConnectedSpace B] : SemilocallySimplyConnectedSpace B

A simply connected space is semilocally simply connected.