feat: port MeasureTheory.Covering.Besicovitch (#4794)

Co-authored-by: Komyyy <pol_tta@outlook.jp>
leanprover-community · Jun 7, 2023 · e715576 · e715576
1 parent 050bf14
commit e715576
Show file tree

Hide file tree

Showing 2 changed files with 1,198 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1991,6 +1991,7 @@ import Mathlib.MeasureTheory.Constructions.Pi
 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.DensityTheorem
 import Mathlib.MeasureTheory.Covering.Differentiation
 import Mathlib.MeasureTheory.Covering.LiminfLimsup