English
If α has a basis of neighborhoods (as above) and each basis element is preconnected, then α is locally connected.
Русский
Если у пространства α имеется база окрестностей из предварительно связанных наборов, то α локально связано.
LaTeX
$$$LocallyConnectedSpace\;\alpha \iff \text{(same basis condition as above)}$$$
Lean4
theorem locallyConnectedSpace [LocallyConnectedSpace α] [TopologicalSpace β] {f : β → α} (h : IsOpenEmbedding f) :
LocallyConnectedSpace β :=
by
refine
locallyConnectedSpace_of_connected_bases (fun _ s ↦ f ⁻¹' s)
(fun x s ↦ (IsOpen s ∧ f x ∈ s ∧ IsConnected s) ∧ s ⊆ range f) (fun x ↦ ?_)
(fun x s hxs ↦ hxs.1.2.2.isPreconnected.preimage_of_isOpenMap h.injective h.isOpenMap hxs.2)
rw [h.nhds_eq_comap]
exact
LocallyConnectedSpace.open_connected_basis (f x) |>.restrict_subset
(h.isOpen_range.mem_nhds <| mem_range_self _) |>.comap
_
