borel_eq_generateFrom — Mathlib

English

Let α be a topological space with a second-countable topology, and s a topological basis for α. Then the Borel sigma-algebra on α equals the sigma-algebra generated by s.

Русский

Пусть α — топологическое пространство со вторичным счетным базисом, и s — топологический базис α. Тогда бореллева сигма-алгебра на α равна сигма-алгебре, порождаемой множеством s.

LaTeX

$$$$ \mathcal{B}(\alpha) = \sigma(s). $$$$

Lean4

theorem borel_eq_generateFrom [TopologicalSpace α] [SecondCountableTopology α] {s : Set (Set α)}
    (hs : IsTopologicalBasis s) : borel α = .generateFrom s :=
  borel_eq_generateFrom_of_subbasis hs.eq_generateFrom

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