isBasis_countableBasis — Mathlib

English

In a second-countable space α, the set countableBasis α itself forms a topological basis for α.

Русский

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

LaTeX

$$$\mathrm{IsTopologicalBasis}(\mathrm{countableBasis}(\alpha))$$$

Lean4

theorem isBasis_countableBasis [SecondCountableTopology α] : IsTopologicalBasis (countableBasis α) :=
  (exists_countable_basis α).choose_spec.2.2

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