class PiBase.SemilocallySimplyConnectedSpace (X : Type u_1) [TopologicalSpace X] : Prop

• homo_trivial (x : X) : ∃ (U : Set X) (hU : U ∈ nhds x), HasTrivialFundGroupImageAt { toFun := Subtype.val, continuous_toFun := ⋯ } ⟨x, ⋯⟩