English
The product of sigma-finite volumes yields a sigma-finite volume on the product space.
Русский
Произведение сигма-ограниченных объёмов даёт сигма-ограниченную меру на произведении.
LaTeX
$$instance prod.instSigmaFinite$$
Lean4
/-- A measure on a product space equals the product measure of sigma-finite measures if they are
equal on rectangles. -/
theorem prod_eq {μ : Measure α} [SigmaFinite μ] {ν : Measure β} [SigmaFinite ν] {μν : Measure (α × β)}
(h : ∀ s t, MeasurableSet s → MeasurableSet t → μν (s ×ˢ t) = μ s * ν t) : μ.prod ν = μν :=
prod_eq_generateFrom generateFrom_measurableSet generateFrom_measurableSet isPiSystem_measurableSet
isPiSystem_measurableSet μ.toFiniteSpanningSetsIn ν.toFiniteSpanningSetsIn fun s hs t ht => h s t hs ht
