Theorem MeasureTheory.lintegral_eq_lintegral_of_isPiSystem_of_univ_mem

Modification history

2025-03-11 20:13
Mathlib/MeasureTheory/Function/AEEqOfLIntegral.lean
feat(MeasureTheory): a.e. equality on product space from equality of integrals (#22764) …
Added MeasureTheory.lintegral_eq_lintegral_of_isPiSystem_of_univ_memView on Github →