English
Let α be a topological space. LocallyConnectedSpace α holds iff for every x ∈ α and every neighborhood U of x, there exists a neighborhood V of x with V ⊆ U and V is preconnected.
Русский
Пусть α — топологическое пространство. Локальная связность α эквивалентна тому, что для каждого x ∈ α и каждой окрестности U(x) существует окрестность V(x) с V ⊆ U и V предварительно связно.
LaTeX
$$$LocallyConnectedSpace\;\alpha \iff \\forall x:\alpha,\forall U \in \mathcal{N}(x),\exists V \in \mathcal{N}(x), IsPreconnected(V) \land V \subseteq U$$$
Lean4
theorem locallyConnectedSpace_iff_connected_subsets :
LocallyConnectedSpace α ↔ ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U :=
by
constructor
· rw [locallyConnectedSpace_iff_subsets_isOpen_isConnected]
intro h x U hxU
rcases h x U hxU with ⟨V, hVU, hV₁, hxV, hV₂⟩
exact ⟨V, hV₁.mem_nhds hxV, hV₂.isPreconnected, hVU⟩
· rw [locallyConnectedSpace_iff_connectedComponentIn_open]
refine fun h U hU x _ => isOpen_iff_mem_nhds.mpr fun y hy => ?_
rw [connectedComponentIn_eq hy]
rcases h y U (hU.mem_nhds <| (connectedComponentIn_subset _ _) hy) with ⟨V, hVy, hV, hVU⟩
exact Filter.mem_of_superset hVy (hV.subset_connectedComponentIn (mem_of_mem_nhds hVy) hVU)
