feat: port MeasureTheory.Function.ConvergenceInMeasure (leanprover-co…

…mmunity#4484) Co-authored-by: Xavier-François Roblot <[email protected]> Co-authored-by: Parcly Taxel <[email protected]>
qawbecrdtey · Jun 12, 2023 · cee1ebf · cee1ebf
1 parent ece218a
commit cee1ebf
Show file tree

Hide file tree

Showing 2 changed files with 370 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1863,6 +1863,7 @@ import Mathlib.MeasureTheory.Decomposition.UnsignedHahn
 import Mathlib.MeasureTheory.Function.AEEqFun
 import Mathlib.MeasureTheory.Function.AEMeasurableOrder
 import Mathlib.MeasureTheory.Function.AEMeasurableSequence
+import Mathlib.MeasureTheory.Function.ConvergenceInMeasure
 import Mathlib.MeasureTheory.Function.Egorov
 import Mathlib.MeasureTheory.Function.EssSup
 import Mathlib.MeasureTheory.Function.Floor