English
The product σ-algebra is generated from boxes, i.e. s × t for sets s ⊆ α and t ⊆ β, where s and t are measurable in their respective spaces.
Русский
Произведение σ-алгебры порождается коробками вида s × t, где s и t измеримы в своих пространствах α и β.
LaTeX
$$$\operatorname{generateFrom}(\{ s \times t \mid s \text{ MeasurableSet in } α,\ t \text{ MeasurableSet in } β \}) = \operatorname{Prod.instMeasurableSpace}$$$
Lean4
/-- The product σ-algebra is generated from boxes, i.e. `s ×ˢ t` for sets `s : Set α` and
`t : Set β`. -/
theorem generateFrom_prod :
generateFrom (image2 (· ×ˢ ·) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t}) =
Prod.instMeasurableSpace :=
generateFrom_eq_prod generateFrom_measurableSet generateFrom_measurableSet isCountablySpanning_measurableSet
isCountablySpanning_measurableSet
