Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-23 09:02 1dafd0f7

View on Github →

feat(measure_theory/integrable_on): a monotone function is integrable on any compact subset (#8336)

Estimated changes

Modified src/measure_theory/integrable_on.lean

added theorem integrable_on_compact_of_antimono

added theorem integrable_on_compact_of_antimono_on

added theorem integrable_on_compact_of_monotone

added theorem integrable_on_compact_of_monotone_on