Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-05 15:05 d40487b5

View on Github →

feat(measure_theory/[set_integral, interval_integral]): mono and nonneg lemmas (#6292) See https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/.60integral_restrict.60/near/226274072

Estimated changes

Modified src/measure_theory/bochner_integration.lean

modified theorem measure_theory.integral_mono

Modified src/measure_theory/interval_integral.lean

added theorem interval_integral.integral_mono

added theorem interval_integral.integral_mono_ae

added theorem interval_integral.integral_mono_ae_restrict

added theorem interval_integral.integral_mono_on

added theorem interval_integral.integral_nonneg

added theorem interval_integral.integral_nonneg_of_ae

added theorem interval_integral.integral_nonneg_of_ae_restrict

Modified src/measure_theory/measure_space.lean

added theorem measure_theory.ae_restrict_of_ae

added theorem measure_theory.ae_restrict_of_ae_restrict_of_subset

Modified src/measure_theory/set_integral.lean

added theorem measure_theory.set_integral_mono

added theorem measure_theory.set_integral_mono_ae

added theorem measure_theory.set_integral_mono_ae_restrict

added theorem measure_theory.set_integral_mono_on

added theorem measure_theory.set_integral_nonneg

added theorem measure_theory.set_integral_nonneg_of_ae

added theorem measure_theory.set_integral_nonneg_of_ae_restrict

Modified test/monotonicity.lean