Theorems · Theorem · measure theory

generateFrom_prod

∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β],
  MeasurableSpace.generateFrom (Set.image2 (fun x1 x2 => x1 ×ˢ x2) {s | MeasurableSet s} {t | MeasurableSet t}) =
    Prod.instMeasurableSpace

The product σ-algebra is generated from boxes, i.e. s ×ˢ t for sets s : Set α and t : Set β.

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Prod

Cited by

11 results in Mathlib

Foundations

Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceMeasurableSpace