English
If α has a basis of neighborhoods b x i at each x, where p x i holds for each i and b x i is preconnected, then α is locally connected.
Русский
Если вдоль каждой точки x пространства α существует база окрестностей {b x i}, такая что каждое b x i предварительно связано и выполняется p x i, то пространство α локально связано.
LaTeX
$$$LocallyConnectedSpace\;\alpha \iff \forall x, (hbasis x).to_hasBasis (\lambda i, i) (\text{subset relation}) (IsPreconnected)\;\Rightarrow \dots$$$
Lean4
theorem locallyConnectedSpace_of_connected_bases {ι : Type*} (b : α → ι → Set α) (p : α → ι → Prop)
(hbasis : ∀ x, (𝓝 x).HasBasis (p x) (b x)) (hconnected : ∀ x i, p x i → IsPreconnected (b x i)) :
LocallyConnectedSpace α := by
rw [locallyConnectedSpace_iff_connected_basis]
exact fun x =>
(hbasis x).to_hasBasis (fun i hi => ⟨b x i, ⟨(hbasis x).mem_of_mem hi, hconnected x i hi⟩, subset_rfl⟩) fun s hs =>
⟨(hbasis x).index s hs.1, ⟨(hbasis x).property_index hs.1, (hbasis x).set_index_subset hs.1⟩⟩
