English
Every locally path-connected space is locally connected.
Русский
Каждое локально путеподключённое пространство локально связно.
LaTeX
$$LocPathConnectedSpace X → LocallyConnectedSpace X$$
Lean4
/-- Locally path-connected spaces are locally connected. -/
instance : LocallyConnectedSpace X :=
by
refine ⟨forall_imp (fun x h ↦ ⟨fun s ↦ ?_⟩) isOpen_isPathConnected_basis⟩
refine ⟨fun hs ↦ ?_, fun ⟨u, ⟨hu, hxu, _⟩, hus⟩ ↦ mem_nhds_iff.mpr ⟨u, hus, hu, hxu⟩⟩
let ⟨u, ⟨hu, hxu, hu'⟩, hus⟩ := (h.mem_iff' s).mp hs
exact ⟨u, ⟨hu, hxu, hu'.isConnected⟩, hus⟩