nonempty_of_mem_countableBasis — Mathlib

English

In a second-countable space, any basis element s in countableBasis α is nonempty.

Русский

В пространстве с двойной счетной топологией любой элемент базиса, принадлежащий countableBasis α, непуст.

LaTeX

$$$\forall \alpha\, [SecondCountableTopology\ \alpha],\; s \in countableBasis(\alpha) \Rightarrow s \neq \emptyset$$$

Lean4

theorem nonempty_of_mem_countableBasis [SecondCountableTopology α] {s : Set α} (hs : s ∈ countableBasis α) :
    s.Nonempty :=
  nonempty_iff_ne_empty.2 <| ne_of_mem_of_not_mem hs <| empty_notMem_countableBasis α

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