English
For μ, ν finite on α × β × γ, μ = ν iff they agree on all products s ×ˢ t ×ˢ u with measurable s, t, u.
Русский
Для конечных меры μ, ν на α × β × γ, μ = ν тогда и только тогда, когда они совпадают на всех продуктах s ×ˢ t ×ˢ u с измеримыми s, t, u.
LaTeX
$$$μ = ν \\iff \\forall {s}:{Set α} {t}:{Set β} {u}:{Set γ},\\; \\text{MeasurableSet}(s) \\to \\text{MeasurableSet}(t) \\to \\text{MeasurableSet}(u) \\to μ(s ×ˢ t ×ˢ u) = ν(s ×ˢ t ×ˢ u)$$$
Lean4
/-- If `s ×ˢ t` is a null measurable set and `ν t ≠ 0`, then `s` is a null measurable set. -/
theorem _root_.MeasureTheory.NullMeasurableSet.left_of_prod {s : Set α} {t : Set β}
(h : NullMeasurableSet (s ×ˢ t) (μ.prod ν)) (ht : ν t ≠ 0) : NullMeasurableSet s μ :=
by
refine .right_of_prod ?_ ht
rw [← preimage_swap_prod]
exact h.preimage measurePreserving_swap.quasiMeasurePreserving
