borel_le_measurable — Mathlib

English

The Borel σ-algebra on ℝ is contained in the Carathéodory σ-algebra generated by the Stieltjes outer measure.

Русский

Borel σ-алгебра на ℝ содержится в Carathéodory σ-алгебре, порожденной внешней мерой Стилетджеса.

LaTeX

$$borel(\mathbb{R}) \subseteq f.outer.caratheodory$$

Lean4

theorem borel_le_measurable : borel ℝ ≤ f.outer.caratheodory :=
  by
  rw [borel_eq_generateFrom_Ioi]
  refine MeasurableSpace.generateFrom_le ?_
  simp +contextual [f.measurableSet_Ioi]

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