instLocallyConnectedSpace — Mathlib

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⟩

Похожие утверждения