Theorem intervalIntegral.norm_integral_le_of_norm_le

Modification history

2025-05-22 09:16
Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean
feat(IntervalIntegral): +1 version of `norm_integral_le_of_norm_le` (#25075)
Added intervalIntegral.norm_integral_le_of_norm_leView on Github →