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

• locally_contractible (x : X) (s : Set X) (h : s ∈ nhds x) : ∃ t ∈ nhds x, ∃ (f : ↑t × ↑unitInterval → X), Continuous f ∧ Set.range f ⊆ s ∧ (∀ (i : ↑t), f (i, 0) = ↑i) ∧ ∀ (i : ↑t), f (i, 1) = x