countablyGenerated — Mathlib

English

If α is a topological space with a second-countable topology, the Borel sigma-algebra on α is countably generated.

Русский

Если α — топологическое пространство со второй счетной топологией, бореллева сигма-алгебра α счётно порождена.

LaTeX

$$$$ \text{CountablyGenerated } \alpha. $$$$

Lean4

instance (priority := 100) countablyGenerated {α : Type*} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α]
    [SecondCountableTopology α] : CountablyGenerated α :=
  by
  obtain ⟨b, bct, -, hb⟩ := exists_countable_basis α
  refine ⟨⟨b, bct, ?_⟩⟩
  borelize α
  exact hb.borel_eq_generateFrom

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