locallyConnectedSpace_iff_connected_basis

English

LocallyConnectedSpace α holds if and only if for every x, the neighborhood filter 𝓝 x has a basis consisting of preconnected sets.

Русский

Локальная связность пространства α эквивалентна тому, что фильтр окрестностей в точке x имеет базис, состоящий из предварительно связных подмножеств.

LaTeX

$$$LocallyConnectedSpace\;\alpha \iff \forall x, (\mathcal{N}x).HasBasis (s:\Set\alpha \to s\in \mathcal{N}x \land IsPreconnected s) \ id$$$

Lean4

theorem locallyConnectedSpace_iff_connected_basis :
    LocallyConnectedSpace α ↔ ∀ x, (𝓝 x).HasBasis (fun s : Set α => s ∈ 𝓝 x ∧ IsPreconnected s) id :=
  by
  rw [locallyConnectedSpace_iff_connected_subsets]
  exact forall_congr' fun x => Filter.hasBasis_self.symm

Похожие утверждения