English
A space is locally path-connected iff every path component of every open subset is open.
Русский
Пространство локально путеподключено тогда и только тогда, когда каждая путевая компонентa любого открытого подмножества открыта.
LaTeX
$$LocPathConnectedSpace X ↔ ∀ x, ∀ u, IsOpen u → IsOpen (pathComponentIn u x)$$
Lean4
/-- A space is locally path-connected iff all path components of open subsets are open. -/
theorem locPathConnectedSpace_iff_isOpen_pathComponentIn {X : Type*} [TopologicalSpace X] :
LocPathConnectedSpace X ↔ ∀ (x : X) (u : Set X), IsOpen u → IsOpen (pathComponentIn u x) :=
⟨fun _ _ _ hu ↦ hu.pathComponentIn _, fun h ↦
⟨fun x ↦
⟨fun s ↦ by
refine ⟨fun hs ↦ ?_, fun ⟨_, ht⟩ ↦ Filter.mem_of_superset ht.1.1 ht.2⟩
let ⟨u, hu⟩ := mem_nhds_iff.mp hs
exact
⟨pathComponentIn u x,
⟨(h x u hu.2.1).mem_nhds (mem_pathComponentIn_self hu.2.2), isPathConnected_pathComponentIn hu.2.2⟩,
pathComponentIn_subset.trans hu.1⟩⟩⟩⟩
