English
If two measures agree on all sets generated by coordinate rectangles, they are equal as product measures.
Русский
Если две меры совпадают на всех множествах, порождённых прямоугольниками координат, то они равны как произведение мер.
LaTeX
$$π μ = μ' if (∀ s, s generates) μ(π univ s) = ∏ μ i(s_i)$$
Lean4
/-- A measure on a finite product space equals the product measure if they are equal on
rectangles. -/
theorem pi_eq [∀ i, SigmaFinite (μ i)] {μ' : Measure (∀ i, α i)}
(h : ∀ s : ∀ i, Set (α i), (∀ i, MeasurableSet (s i)) → μ' (pi univ s) = ∏ i, μ i (s i)) : Measure.pi μ = μ' :=
pi_eq_generateFrom (fun _ => generateFrom_measurableSet) (fun _ => isPiSystem_measurableSet)
(fun i => (μ i).toFiniteSpanningSetsIn) h
