mathlib3
3a0f2822 - feat(measure_theory/interval_integral): integral of a non-integrable function (#8011)

Commit

4 years ago

feat(measure_theory/interval_integral): integral of a non-integrable function (#8011) The `interval_integral` of a non-`interval_integrable` function is `0`.

Author

benjamindavidson

Parents

7d155d95

mathlib3 3a0f2822 - feat(measure_theory/interval_integral): integral of a non-integrable function (#8011)

mathlib3
3a0f2822 - feat(measure_theory/interval_integral): integral of a non-integrable function (#8011)