English
Two finite measures μ and ν on α × β × γ are equal if and only if they agree on all products of sets of the form s × t × u with s ⊆ α, t ⊆ β, u ⊆ γ measurable.
Русский
Две конечные меры μ и ν на α × β × γ равны тогда и только тогда, когда они совпадают на всех произведениях множеств вида s × t × u с измеримыми s ⊆ α, t ⊆ β, u ⊆ γ.
LaTeX
$$$μ = ν \\iff \\forall s,t,u,\\; \\text{MeasurableSet}(s) \\to \\text{MeasurableSet}(t) \\to \\text{MeasurableSet}(u) \\to μ(s ×ˢ t ×ˢ u) = ν(s ×ˢ t ×ˢ u)$$$
Lean4
/-- Two finite measures on a product `α × β × γ` are equal iff they are equal on products of sets.
See `ext_prod₃_iff'` for the same statement for `(α × β) × γ`. -/
theorem ext_prod₃_iff {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
{μ ν : Measure (α × β × γ)} [IsFiniteMeasure μ] :
μ = ν ↔
(∀ {s : Set α} {t : Set β} {u : Set γ},
MeasurableSet s → MeasurableSet t → MeasurableSet u → μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)) :=
⟨fun h s t u hs ht hu ↦ by rw [h], Measure.ext_prod₃⟩
