Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-27 23:02 a445c45c

View on Github →

feat(measure_theory/interval_integrable): a monotone function is interval integrable (#8398)

Estimated changes

Modified src/measure_theory/interval_integral.lean

added theorem interval_integrable_of_antimono

added theorem interval_integrable_of_antimono_on

added theorem interval_integrable_of_monotone

added theorem interval_integrable_of_monotone_on