class PiBase.SemilocallyContractibleSpace (X : Type u) [TopologicalSpace X] : Prop

• contractible_nbhd (x : X) : ∃ s ∈ nhds x, ∃ (f : ↑unitInterval → ↑s → X), Continuous (Function.uncurry f) ∧ f 0 = Subtype.val ∧ ∀ (a b : ↑s), f 1 a = f 1 b