Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-15 23:35 30314c22

View on Github →

fix(measure_theory/interval_integral): generalize some lemmas (#7944) The proofs of some lemmas about the integral of a function f : ℝ → ℝ also hold for f : α → ℝ (with α under the usual conditions).

Estimated changes

Modified src/analysis/special_functions/integrals.lean

modified theorem integral_sin_pow_antimono

Modified src/measure_theory/interval_integral.lean

modified theorem interval_integral.integral_eq_zero_iff_of_le_of_nonneg_ae

modified theorem interval_integral.integral_eq_zero_iff_of_nonneg_ae

modified theorem interval_integral.integral_mono_ae_restrict

modified theorem interval_integral.integral_mono_on

modified theorem interval_integral.integral_nonneg

modified theorem interval_integral.integral_nonneg_of_ae

modified theorem interval_integral.integral_nonneg_of_ae_restrict

modified theorem interval_integral.integral_pos_iff_support_of_nonneg_ae'

modified theorem interval_integral.integral_pos_iff_support_of_nonneg_ae