borel_eq_generateFrom_Ioo_rat — Mathlib

English

The Borel σ-algebra on the real numbers is generated by the open intervals with rational endpoints.

Русский

Борелева σ-алгебра на действительных числах порождается открытыми интервалами с рациональными границами.

LaTeX

$$borel ℝ = generateFrom (⋃ (a : ℚ) (b : ℚ) (a < b), {Ioo (a : ℝ) (b : ℝ)})$$

Lean4

theorem borel_eq_generateFrom_Ioo_rat :
    borel ℝ = .generateFrom (⋃ (a : ℚ) (b : ℚ) (_ : a < b), {Ioo (a : ℝ) (b : ℝ)}) :=
  isTopologicalBasis_Ioo_rat.borel_eq_generateFrom

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