borel_eq_generateFrom_isClosed — Mathlib

English

The Borel sigma-algebra is generated by the family of closed sets: borel α = generateFrom {s | IsClosed s}.

Русский

Бореллева сигма-алгебра порождается семейством замкнутых множеств: бореллева сигма-алгебра α равна generateFrom{ s | IsClosed s }.

LaTeX

$$$$ \mathrm{borel}(\alpha) = \mathrm{generateFrom}\{s \mid IsClosed(s)\}. $$$$

Lean4

theorem borel_eq_generateFrom_isClosed [TopologicalSpace α] : borel α = .generateFrom {s | IsClosed s} :=
  le_antisymm
    (generateFrom_le fun _t ht =>
      @MeasurableSet.of_compl α _ (generateFrom {s | IsClosed s})
        (GenerateMeasurable.basic _ <| isClosed_compl_iff.2 ht))
    (generateFrom_le fun _t ht =>
      @MeasurableSet.of_compl α _ (borel α) (GenerateMeasurable.basic _ <| isOpen_compl_iff.2 ht))

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