Commit 2021-05-24 14:07 a09ddc7f

View on Github →

feat(measure_theory/interval_integral): interval_integrable.mono (#7679) interval_integrable f ν a b → interval c d ⊆ interval a b → μ ≤ ν → interval_integrable f μ c d

Estimated changes

Modified src/measure_theory/interval_integral.lean

added theorem interval_integrable.def

added theorem interval_integrable.mono

added theorem interval_integrable.mono_measure

added theorem interval_integrable.mono_set

added theorem interval_integrable.mono_set_ae

modified theorem interval_integrable.trans

added theorem interval_integrable_iff

modified theorem measure_theory.integrable.interval_integrable