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