feat: port MeasureTheory.Covering.Vitali (#4178)

leanprover-community · May 22, 2023 · 6453a95 · 6453a95
1 parent e23d258
commit 6453a95
Show file tree

Hide file tree

Showing 2 changed files with 448 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1678,6 +1678,7 @@ import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
 import Mathlib.MeasureTheory.Constructions.BorelSpace.Complex
 import Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap
 import Mathlib.MeasureTheory.Constructions.Polish
+import Mathlib.MeasureTheory.Covering.Vitali
 import Mathlib.MeasureTheory.Covering.VitaliFamily
 import Mathlib.MeasureTheory.Decomposition.UnsignedHahn
 import Mathlib.MeasureTheory.Function.AEMeasurableOrder