borel_eq_generateFrom_Ici_rat — Mathlib

English

The real Borel sigma-algebra is generated by the closed rays [a, ∞) with rational a. Equivalently, Borel(ℝ) = generateFrom(⋃_{a ∈ ℚ} {Ici(a)}).

Русский

Борелева сигма-алгебра на ℝ порождается множествами [a, ∞) при рациональных a. Иными словами, Borel(ℝ) = generateFrom(⋃_{a ∈ ℚ} {Ici(a)}).

LaTeX

$$$$\operatorname{borel}(\mathbb{R}) = \operatorname{generateFrom}\left(\bigcup_{a \in \mathbb{Q}} \{ Ici(a) \} \right)$$$$

Lean4

theorem borel_eq_generateFrom_Ici_rat : borel ℝ = .generateFrom (⋃ a : ℚ, {Ici (a : ℝ)}) :=
  by
  rw [borel_eq_generateFrom_Iio_rat, iUnion_singleton_eq_range, iUnion_singleton_eq_range]
  refine le_antisymm (generateFrom_le ?_) (generateFrom_le ?_) <;> rintro _ ⟨q, rfl⟩ <;> dsimp only <;>
      [rw [← compl_Ici]; rw [← compl_Iio]] <;>
    exact MeasurableSet.compl (GenerateMeasurable.basic _ (mem_range_self q))

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