Minimize imports

leanprover-community · Oct 29, 2024 · 00af82f · 00af82f
1 parent ae9a0c1
commit 00af82f
Showing 1 changed file with 1 addition and 3 deletions.
diff --git a/Mathlib/Topology/Algebra/Order/LiminfLimsup.lean b/Mathlib/Topology/Algebra/Order/LiminfLimsup.lean
@@ -8,11 +8,9 @@ import Mathlib.Algebra.BigOperators.Ring
 import Mathlib.Algebra.Order.Group.DenselyOrdered
 import Mathlib.Algebra.Order.Group.Indicator
 import Mathlib.Data.Real.Archimedean
-import Mathlib.Order.LiminfLimsup
 import Mathlib.Order.Filter.AtTopBot.Archimedean
-import Mathlib.Order.Filter.CountableInter
+import Mathlib.Order.LiminfLimsup
 import Mathlib.Topology.Algebra.Group.Basic
-import Mathlib.Data.Set.Lattice
 import Mathlib.Topology.Order.Monotone
 
 /-!