English
Let α be a topological space. Locally connectedSpace α holds if and only if for every open subset F of α and every x in F, the connected component of x in F is open in α.
Русский
Пусть α — топологическое пространство. Локальная связность α эквивалентна тому, что для каждого открытого подмножества F ⊆ α и каждого x ∈ F связная компонента x внутри F является открытым подмножество α.
LaTeX
$$$LocallyConnectedSpace\;\alpha \iff \forall F \subseteq \alpha,\ IsOpen(F) \to \forall x \in F,\ IsOpen(connectedComponentIn F x) $$$
Lean4
theorem locallyConnectedSpace_iff_connectedComponentIn_open :
LocallyConnectedSpace α ↔ ∀ F : Set α, IsOpen F → ∀ x ∈ F, IsOpen (connectedComponentIn F x) :=
by
constructor
· intro h
exact fun F hF x _ => hF.connectedComponentIn
· intro h
rw [locallyConnectedSpace_iff_subsets_isOpen_isConnected]
refine fun x U hU =>
⟨connectedComponentIn (interior U) x, (connectedComponentIn_subset _ _).trans interior_subset,
h _ isOpen_interior x ?_, mem_connectedComponentIn ?_, isConnected_connectedComponentIn_iff.mpr ?_⟩ <;>
exact mem_interior_iff_mem_nhds.mpr hU
