tidy imports

fpvandoorn · Sep 21, 2024 · 17a75a1 · 17a75a1
1 parent cd5d125
commit 17a75a1
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 2 deletions.
diff --git a/Carleson/Discrete/ForestComplement.lean b/Carleson/Discrete/ForestComplement.lean
@@ -1,5 +1,4 @@
 import Carleson.Discrete.Defs
-import Carleson.Forest
 import Mathlib.Combinatorics.Enumerative.DoubleCounting
 
 open MeasureTheory Measure NNReal Metric Complex Set

diff --git a/Carleson/Discrete/ForestUnion.lean b/Carleson/Discrete/ForestUnion.lean
@@ -1,7 +1,6 @@
 import Carleson.Discrete.ExceptionalSet
 import Carleson.Discrete.ForestComplement
 import Carleson.Forest
-import Mathlib.Combinatorics.Enumerative.DoubleCounting
 
 open MeasureTheory Measure NNReal Metric Complex Set
 open scoped ENNReal