Commit 2025-03-11 20:13 c2afb774

feat(MeasureTheory): a.e. equality on product space from equality of integrals (#22764) If two a.e.-measurable functions α × β → ℝ≥0∞ with finite integrals have the same integral on every rectangle, then they are almost everywhere equal. The new result puts together the fact that a.e.-equality can be proven from equality of integrals, and induction over the pi-system of rectangles.