measurableSpace_iSup_eq — Mathlib

English

The supremum of a family of σ-algebras m: ι → MeasurableSpace α is equal to the σ-algebra generated by the sets that are measurable in some m i; i.e., ⨆ i m i = GenerateFrom { s ⊆ α | ∃ i, MeasurableSet[m i] s }.

Русский

Наибольшая верхняя граница семейства σ‑алгебр m i равна σ-алгебе, порождаемой множеством { s ⊆ α | ∃ i, MeasurableSet[m i] s }.

LaTeX

$$$\\bigvee_{i} m(i) = \\mathrm{generateFrom}\\{ s \\subseteq \\alpha \\;|\\; \\exists i, \\text{MeasurableSet}[m(i)]\\; s \\}$.$$

Lean4

theorem measurableSpace_iSup_eq (m : ι → MeasurableSpace α) : ⨆ n, m n = generateFrom {s | ∃ n, MeasurableSet[m n] s} :=
  by
  ext s
  rw [measurableSet_iSup]
  rfl

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