Theorem exists_eq_const_mul_setIntegral_of_nonneg

Modification history

2026-01-05 16:12
Mathlib/MeasureTheory/Integral/MeanValue.lean
feat(MeasureTheory/Integral): add versions of `exists_eq_interval_average` and first mean value theorem for integrals (#30344) …
Added exists_eq_const_mul_setIntegral_of_nonnegView on Github →