Theorem MeasureTheory.lintegral_eq_iff_ae_eq_of_ae_le

Modification history

2026-09-08 18:35
Mathlib/MeasureTheory/Integral/Lebesgue/Markov.lean
feat(MeasureTheory/Integral/MeanInequalities): strict Hölder's inequality for Lebesgue integrals (#40851) …
Added MeasureTheory.lintegral_eq_iff_ae_eq_of_ae_leView on Github →