toSecondCountableTopology — Mathlib

English

If α is finite, then α is automatically second-countable.

Русский

Если множество α конечное, то любая топология на α делает его вторую счётность.

LaTeX

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

Lean4

instance _root_.Finite.toSecondCountableTopology [Finite α] : SecondCountableTopology α where
  is_open_generated_countable :=
    ⟨_, {U | IsOpen U}.to_countable, TopologicalSpace.isTopologicalBasis_opens.eq_generateFrom⟩

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