From 00af82f2dabbe5a4099f01838043b36271aa9487 Mon Sep 17 00:00:00 2001 From: D-Thomine <100795491+D-Thomine@users.noreply.github.com> Date: Tue, 29 Oct 2024 02:16:46 +0100 Subject: [PATCH] Minimize imports --- Mathlib/Topology/Algebra/Order/LiminfLimsup.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Mathlib/Topology/Algebra/Order/LiminfLimsup.lean b/Mathlib/Topology/Algebra/Order/LiminfLimsup.lean index d13fd03208799..d4c75cfae42d7 100644 --- 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 /-!