English
LocPathConnectedSpace X is equivalent to the property that for all x and all open u, pathComponentIn u x is open.
Русский
Локальная путеподключенность эквивалентна свойству: для всех x и всех открытых u путь-компонента x в u открыта.
LaTeX
$$locPathConnectedSpace_iff_isOpen_pathComponentIn$$
Lean4
/-- A space is locally path-connected iff all path components of open subsets are neighbourhoods. -/
theorem locPathConnectedSpace_iff_pathComponentIn_mem_nhds {X : Type*} [TopologicalSpace X] :
LocPathConnectedSpace X ↔ ∀ x : X, ∀ u : Set X, IsOpen u → x ∈ u → pathComponentIn u x ∈ nhds x :=
by
rw [locPathConnectedSpace_iff_isOpen_pathComponentIn]
simp_rw [forall_comm (β := Set X), ← imp_forall_iff]
refine forall_congr' fun u ↦ imp_congr_right fun _ ↦ ?_
exact
⟨fun h x hxu ↦ (h x).mem_nhds (mem_pathComponentIn_self hxu), fun h x ↦
isOpen_iff_mem_nhds.mpr fun y hy ↦ pathComponentIn_congr hy ▸ h y <| pathComponentIn_subset hy⟩
