feat: port MeasureTheory.Function.L1Space (#4383)

leanprover-community · May 31, 2023 · 27ebbd6 · 27ebbd6
1 parent d90140d
commit 27ebbd6
Show file tree

Hide file tree

Showing 3 changed files with 1,451 additions and 1 deletion.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1856,6 +1856,7 @@ import Mathlib.MeasureTheory.Function.AEMeasurableSequence
 import Mathlib.MeasureTheory.Function.Egorov
 import Mathlib.MeasureTheory.Function.EssSup
 import Mathlib.MeasureTheory.Function.Floor
+import Mathlib.MeasureTheory.Function.L1Space
 import Mathlib.MeasureTheory.Function.LpOrder
 import Mathlib.MeasureTheory.Function.LpSeminorm
 import Mathlib.MeasureTheory.Function.LpSpace