locallyConnectedSpace_iff_hasBasis_isOpen_isConnected

English

LocallyConnectedSpace α is equivalent to the existence of a basis of nhds consisting of open connected sets around each point.

Русский

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

LaTeX

$$LocallyConnectedSpace α ↔ ∀ x, (nhds x).HasBasis (fun s => IsOpen s ∧ x ∈ s ∧ IsConnected s) id$$

Lean4

theorem locallyConnectedSpace_iff_hasBasis_isOpen_isConnected :
    LocallyConnectedSpace α ↔ ∀ x, (𝓝 x).HasBasis (fun s : Set α => IsOpen s ∧ x ∈ s ∧ IsConnected s) id :=
  ⟨@LocallyConnectedSpace.open_connected_basis _ _, LocallyConnectedSpace.mk⟩

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