Mathlib v3 is deprecated. Go to Mathlib v4

Theorem interval_integral.abs_integral_le_integral_abs

Modification history

2021-12-28 11:35

src/measure_theory/integral/interval_integral.lean

feat(measure_theory/integral/{interval,circle}_integral): add strict inequalities (#11061)

Modified interval_integral.abs_integral_le_integral_abs View on Github →

2021-06-19 15:31

src/measure_theory/interval_integral.lean

feat(measure_theory/interval_integral): `abs_integral_le_integral_abs` (#7959) …

Added interval_integral.abs_integral_le_integral_abs View on Github →