feat: port MeasureTheory.Function.LocallyIntegrable (#4524)

leanprover-community · Jun 1, 2023 · 77ba888 · 77ba888
1 parent 54965d9
commit 77ba888
Show file tree

Hide file tree

Showing 2 changed files with 485 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1864,6 +1864,7 @@ import Mathlib.MeasureTheory.Function.Egorov
 import Mathlib.MeasureTheory.Function.EssSup
 import Mathlib.MeasureTheory.Function.Floor
 import Mathlib.MeasureTheory.Function.L1Space
+import Mathlib.MeasureTheory.Function.LocallyIntegrable
 import Mathlib.MeasureTheory.Function.LpOrder
 import Mathlib.MeasureTheory.Function.LpSeminorm
 import Mathlib.MeasureTheory.Function.LpSpace