feat: port MeasureTheory.Decomposition.Lebesgue (#4736)

leanprover-community · Jun 7, 2023 · aab87ec · aab87ec
1 parent 159e04e
commit aab87ec
Show file tree

Hide file tree

Showing 2 changed files with 1,249 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1981,6 +1981,7 @@ import Mathlib.MeasureTheory.Constructions.Prod.Integral
 import Mathlib.MeasureTheory.Covering.Vitali
 import Mathlib.MeasureTheory.Covering.VitaliFamily
 import Mathlib.MeasureTheory.Decomposition.Jordan
+import Mathlib.MeasureTheory.Decomposition.Lebesgue
 import Mathlib.MeasureTheory.Decomposition.SignedHahn
 import Mathlib.MeasureTheory.Decomposition.UnsignedHahn
 import Mathlib.MeasureTheory.Function.AEEqFun