English
The Borel sigma-algebra on the real line is generated by the open rays (a, ∞) as a ranges over all rational numbers. In other words, Borel(ℝ) is the sigma-algebra generated by the collection { (a, ∞) | a ∈ ℚ }.
Русский
Борелева сигма-алгебра на ℝ порождается множествами (a, ∞) при рациональных a. То есть Borel(ℝ) генерируется коллекцией { (a, ∞) : a ∈ ℚ }.
LaTeX
$$$$\\operatorname{borel}(\\mathbb{R}) = \\operatorname{generateFrom}\\left(\\bigcup_{a \\in \\mathbb{Q}} \\{\,Ioi(a)\\,\}\\right)$$$$
Lean4
theorem borel_eq_generateFrom_Ioi_rat : borel ℝ = .generateFrom (⋃ a : ℚ, {Ioi (a : ℝ)}) :=
by
rw [borel_eq_generateFrom_Ioi]
refine
le_antisymm (generateFrom_le ?_)
(generateFrom_mono <| iUnion_subset fun q ↦ singleton_subset_iff.mpr <| mem_range_self _)
rintro _ ⟨a, rfl⟩
have : IsGLB (range ((↑) : ℚ → ℝ) ∩ Ioi a) a := by
simp [isGLB_iff_le_iff, mem_lowerBounds, ← le_iff_forall_lt_rat_imp_le]
rw [← this.biUnion_Ioi_eq, ← image_univ, ← image_inter_preimage, univ_inter, biUnion_image]
exact MeasurableSet.biUnion (to_countable _) fun b _ => GenerateMeasurable.basic (Ioi (b : ℝ)) (by simp)
