feat: port MeasureTheory.Integral.IntegrableOn (#4520)

leanprover-community · May 31, 2023 · 19f958e · 19f958e
1 parent e9bc920
commit 19f958e
Show file tree

Hide file tree

Showing 2 changed files with 713 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1876,6 +1876,7 @@ import Mathlib.MeasureTheory.Group.MeasurableEquiv
 import Mathlib.MeasureTheory.Group.Measure
 import Mathlib.MeasureTheory.Group.Pointwise
 import Mathlib.MeasureTheory.Group.Prod
+import Mathlib.MeasureTheory.Integral.IntegrableOn
 import Mathlib.MeasureTheory.Integral.Lebesgue
 import Mathlib.MeasureTheory.Integral.LebesgueNormedSpace
 import Mathlib.MeasureTheory.Integral.MeanInequalities