to_separableSpace — Mathlib

English

A second-countable space is separable.

Русский

Вторично счетное пространство является сепарабельным.

LaTeX

$$$\text{SecondCountableTopology}(\alpha) \Rightarrow \text{SeparableSpace}(\alpha)$$$

Lean4

instance (priority := 100) to_separableSpace [SecondCountableTopology α] : SeparableSpace α :=
  by
  choose p hp using fun s : countableBasis α => nonempty_of_mem_countableBasis s.2
  exact
    ⟨⟨range p, countable_range _,
        (isBasis_countableBasis α).dense_iff.2 fun o ho _ => ⟨p ⟨o, ho⟩, hp ⟨o, _⟩, mem_range_self _⟩⟩⟩

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