feat: port MeasureTheory.Covering.BesicovitchVectorSpace (#4832)

leanprover-community · Jun 8, 2023 · d217949 · d217949
1 parent 6101723
commit d217949
Show file tree

Hide file tree

Showing 2 changed files with 558 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1997,6 +1997,7 @@ import Mathlib.MeasureTheory.Constructions.Polish
 import Mathlib.MeasureTheory.Constructions.Prod.Basic
 import Mathlib.MeasureTheory.Constructions.Prod.Integral
 import Mathlib.MeasureTheory.Covering.Besicovitch
+import Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
 import Mathlib.MeasureTheory.Covering.DensityTheorem
 import Mathlib.MeasureTheory.Covering.Differentiation
 import Mathlib.MeasureTheory.Covering.LiminfLimsup