English
The Borel σ-algebra on ℝ equals the generateFrom of sets Iio with rational endpoints.
Русский
Борелeва σ-алгебра на ℝ равна σ-порожденной ∪ Iio рациональных концов.
LaTeX
$$borel ℝ = .generateFrom (⋃ a : ℚ, {Iio (a : ℝ)})$$
Lean4
theorem borel_eq_generateFrom_Iio_rat : borel ℝ = .generateFrom (⋃ a : ℚ, {Iio (a : ℝ)}) :=
by
rw [borel_eq_generateFrom_Iio]
refine
le_antisymm (generateFrom_le ?_)
(generateFrom_mono <| iUnion_subset fun q ↦ singleton_subset_iff.mpr <| mem_range_self _)
rintro _ ⟨a, rfl⟩
have : IsLUB (range ((↑) : ℚ → ℝ) ∩ Iio a) a := by
simp [isLUB_iff_le_iff, mem_upperBounds, ← le_iff_forall_rat_lt_imp_le]
rw [← this.biUnion_Iio_eq, ← image_univ, ← image_inter_preimage, univ_inter, biUnion_image]
exact MeasurableSet.biUnion (to_countable _) fun b _ => GenerateMeasurable.basic (Iio (b : ℝ)) (by simp)