interval_integral): add lemma `interval_integrable.sum` (#14069)

Commit

3 years ago

feat(measure_theory/integral/interval_integral): add lemma `interval_integrable.sum` (#14069) Formalized as part of the Sphere Eversion project.

Author

ocfnash

Parents