borel_eq_generateFrom_Iio_rat — Mathlib

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)

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