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

• contractible_nbhd {x : X} {N : Set X} (hN : N ∈ nhds x) : ∃ (U : Set ↑N), IsPathConnected U ∧ ∃ (hU : U ∈ nhds ⟨x, ⋯⟩), HasTrivialFundGroupImageAt { toFun := Subtype.val, continuous_toFun := ⋯ } ⟨⟨x, ⋯⟩, ⋯⟩