Commit 2021-12-26 03:49 dd6707c9

View on Github →

feat(measure_theory/integral): a couple of lemmas on integrals and integrability (#10983) Adds a couple of congruence lemmas for integrating on intervals and integrability

Estimated changes

Modified src/measure_theory/integral/integrable_on.lean

added theorem measure_theory.integrable_on.congr_fun'

added theorem measure_theory.integrable_on.congr_fun

Modified src/measure_theory/integral/interval_integral.lean

deleted theorem interval_integral.integral_Icc_eq_integral_Ioc'

deleted theorem interval_integral.integral_Icc_eq_integral_Ioc

Modified src/measure_theory/integral/set_integral.lean

added theorem measure_theory.integral_Icc_eq_integral_Ioc'

added theorem measure_theory.integral_Icc_eq_integral_Ioc

added theorem measure_theory.integral_Ioc_eq_integral_Ioo'

added theorem measure_theory.integral_Ioc_eq_integral_Ioo

Modified src/measure_theory/measure/measure_space.lean

added theorem measure_theory.Ico_ae_eq_Icc'

added theorem measure_theory.Ico_ae_eq_Ioc'

added theorem measure_theory.Iio_ae_eq_Iic'

added theorem measure_theory.Ioc_ae_eq_Icc'

added theorem measure_theory.Ioi_ae_eq_Ici'

added theorem measure_theory.Ioo_ae_eq_Icc'

added theorem measure_theory.Ioo_ae_eq_Ico'

added theorem measure_theory.Ioo_ae_eq_Ioc'