generateFrom_pi — Mathlib

English

The product σ-algebra is generated by boxes, i.e., by sets of the form A×B with A,B measurable.

Русский

Произведение σ-алгебр генерируется коробками, т. е. множествами вида A×B, где A,B измеримы.

LaTeX

$$$\\mathrm{generateFrom}(\\{\\{s: \\mathrm{Set}(\\alpha) : \\mathrm{MeasurableSet}(s)\\} \\}) = \\mathrm{pi}$$$

Lean4

/-- The product σ-algebra is generated from boxes, i.e. `s ×ˢ t` for sets `s : set α` and
  `t : set β`. -/
theorem generateFrom_pi [∀ i, MeasurableSpace (α i)] :
    generateFrom (pi univ '' pi univ fun i => {s : Set (α i) | MeasurableSet s}) = MeasurableSpace.pi :=
  generateFrom_eq_pi (fun _ => generateFrom_measurableSet) fun _ => isCountablySpanning_measurableSet

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