English
The real Borel sigma-algebra is generated by the closed rays (−∞, a] with rational endpoints a. Equivalently, Borel(ℝ) = generateFrom(⋃_{a ∈ ℚ} {Iic(a)}).
Русский
Борелева сигма-алгебра на ℝ порождается множествами (−∞, a] при рациональных a. Иными словами, Borel(ℝ) = generateFrom(⋃_{a ∈ ℚ} {Iic(a)}).
LaTeX
$$$$\operatorname{borel}(\mathbb{R}) = \operatorname{generateFrom}\left(\bigcup_{a \in \mathbb{Q}} \{ Iic(a) \} \right)$$$$
Lean4
theorem borel_eq_generateFrom_Iic_rat : borel ℝ = .generateFrom (⋃ a : ℚ, {Iic (a : ℝ)}) :=
by
rw [borel_eq_generateFrom_Ioi_rat, iUnion_singleton_eq_range, iUnion_singleton_eq_range]
refine le_antisymm (generateFrom_le ?_) (generateFrom_le ?_) <;> rintro _ ⟨q, rfl⟩ <;> dsimp only <;>
[rw [← compl_Iic]; rw [← compl_Ioi]] <;>
exact MeasurableSet.compl (GenerateMeasurable.basic _ (mem_range_self q))
