English
LocallyConnectedSpace α is equivalent to the basis condition: for every x, nhds x has a basis of open connected sets containing x.
Русский
Локальная связность пространства эквивалентна условию базиса: для каждого x окрестности имеют базис открытых связных множеств, содержащихся в x.
LaTeX
$$LocallyConnectedSpace α ↔ ∀ x, (nhds x).HasBasis (fun s => IsOpen s ∧ x ∈ s ∧ IsConnected s) id$$
Lean4
theorem locallyConnectedSpace_iff_subsets_isOpen_isConnected :
LocallyConnectedSpace α ↔ ∀ x, ∀ U ∈ 𝓝 x, ∃ V : Set α, V ⊆ U ∧ IsOpen V ∧ x ∈ V ∧ IsConnected V :=
by
simp_rw [locallyConnectedSpace_iff_hasBasis_isOpen_isConnected]
refine forall_congr' fun _ => ?_
constructor
· intro h U hU
rcases h.mem_iff.mp hU with ⟨V, hV, hVU⟩
exact ⟨V, hVU, hV⟩
·
exact fun h =>
⟨fun U =>
⟨fun hU =>
let ⟨V, hVU, hV⟩ := h U hU
⟨V, hV, hVU⟩,
fun ⟨V, ⟨hV, hxV, _⟩, hVU⟩ => mem_nhds_iff.mpr ⟨V, hVU, hV, hxV⟩⟩⟩