Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-23 13:11 28177886

View on Github →

chore(measure_theory/integral): add integrable_const for interval_integral (#10410)

Estimated changes

Modified src/measure_theory/integral/integrable_on.lean

modified theorem measure_theory.integrable_on_const

Modified src/measure_theory/integral/interval_integral.lean

added theorem interval_integrable_const

added theorem interval_integrable_const_iff

Modified src/measure_theory/measure/measure_space.lean