Commit 2021-04-11 10:03 1442f70a

View on Github →

feat(measure_theory/interval_integral): variants of integral_comp lemmas (#7103) Alternate versions of some of our integral_comp lemmas which work even when c = 0.

Estimated changes

Modified src/measure_theory/interval_integral.lean

added theorem interval_integral.integral_comp_add_div'

modified theorem interval_integral.integral_comp_add_div

added theorem interval_integral.integral_comp_add_mul'

modified theorem interval_integral.integral_comp_add_mul

modified theorem interval_integral.integral_comp_add_right

added theorem interval_integral.integral_comp_div'

added theorem interval_integral.integral_comp_div_add'

modified theorem interval_integral.integral_comp_div_add

added theorem interval_integral.integral_comp_div_sub'

modified theorem interval_integral.integral_comp_div_sub

added theorem interval_integral.integral_comp_mul_add'

modified theorem interval_integral.integral_comp_mul_add

added theorem interval_integral.integral_comp_mul_left'

added theorem interval_integral.integral_comp_mul_right'

added theorem interval_integral.integral_comp_mul_sub'

modified theorem interval_integral.integral_comp_mul_sub

added theorem interval_integral.integral_comp_sub_div'

modified theorem interval_integral.integral_comp_sub_div

modified theorem interval_integral.integral_comp_sub_left

added theorem interval_integral.integral_comp_sub_mul'

modified theorem interval_integral.integral_comp_sub_mul

modified theorem interval_integral.integral_comp_sub_right