exists_countable_basis — Mathlib

English

In a second-countable space α, there exists a countable set of open sets that forms a topological basis for α.

Русский

В пространстве α со второй счётностью существует счётное множество открытых множеств, образующее топологический базис.

LaTeX

$$$\exists b:\, b.cntable \land ∅ \not\in b \land IsTopologicalBasis b$$$

Lean4

theorem exists_countable_basis [SecondCountableTopology α] :
    ∃ b : Set (Set α), b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b :=
  by
  obtain ⟨b, hb₁, hb₂⟩ := @SecondCountableTopology.is_open_generated_countable α _ _
  refine ⟨_, ?_, notMem_diff_of_mem ?_, (isTopologicalBasis_of_subbasis hb₂).diff_empty⟩
  exacts [((countable_setOf_finite_subset hb₁).image _).mono diff_subset, rfl]

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