theorem fubini_theorem {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : α × β → E) (hf : MeasureTheory.Integrable f (μ.prod ν)) : ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ ∧ ∫ (z : α × β), f z ∂μ.prod ν = ∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν ∧ ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ = ∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν

Fubini's theorem. For σ-finite (here SFinite) measures μ on α and ν on β and a function f : α × β → E that is integrable w.r.t. the product measure μ.prod ν, the integral of f over the product space agrees with both iterated integrals, and the two iterated integrals agree with each other: ∫_{α × β} f d(μ × ν) = ∫_α ∫_β f(x,y) dν dμ = ∫_β ∫_α f(x,y) dμ dν.