Reduce imports

Author: nguyenvukhang

Rudin/Partition/Core/Index.lean

@@ -1,4 +1,3 @@
-import Rudin.Defs.Partition
 import Rudin.Partition.Core.Endpoints
 import Rudin.Partition.Core.Monotone
 

Rudin/Partition/Core/Length.lean

@@ -1,5 +1,3 @@
-import Mathlib.Data.Finset.Card
-
 import Rudin.Defs.Partition
 
 namespace Rudin

Rudin/Partition/Core/Monotone.lean

@@ -1,4 +1,4 @@
-import Rudin.Partition.Core.Length
+import Rudin.Defs.Partition
 
 namespace Rudin
 

Rudin/Partition/Cover.lean

@@ -1,6 +1,7 @@
 import Mathlib.Data.Set.Lattice
 import Mathlib.Order.Interval.Set.LinearOrder
 
+import Rudin.Partition.Core
 import Rudin.Partition.Endpoints
 
 namespace Rudin

Rudin/Partition/Endpoints.lean

@@ -1,4 +1,4 @@
-import Rudin.Partition.Core
+import Rudin.Partition.Core.Index
 import Rudin.Partition.Monotone
 
 namespace Rudin

Rudin/Partition/Insert.lean

@@ -1,9 +1,6 @@
-import Mathlib.Data.Set.Lattice
-import Mathlib.Order.Interval.Set.LinearOrder
-
-import Rudin.Partition.Endpoints
 import Rudin.Partition.Prelude
-import Rudin.Partition.OrderBot
+import Rudin.Partition.Core.Length
+import Rudin.Partition.Endpoints
 
 namespace Rudin
 

Rudin/Partition/Interval.lean

@@ -1,4 +1,5 @@
 import Rudin.Partition.Endpoints
+import Rudin.Partition.Core
 import Rudin.Prelude
 
 open Set

Rudin/Partition/OrderBot.lean

@@ -1,4 +1,5 @@
 import Rudin.Partition.Endpoints
+import Rudin.Partition.Core
 import Mathlib.Tactic
 
 namespace Rudin

Rudin/Prelude/BddOn.lean

@@ -1,8 +1,6 @@
 /-
 This file introduces BddOn, which is BddAbove ∧ BddBelow
 -/
-import Mathlib.Data.Real.Basic
-import Mathlib.Order.ConditionallyCompleteLattice.Defs
 import Mathlib.Data.Real.Archimedean
 
 universe u v
@@ -218,7 +216,7 @@ theorem BddOn.sInf_le_sSup (s : BddOn f A) : sInf (f '' A) ≤ sSup (f '' A)
 
 end RealValuedFunctions
 --------------------------------------------------------------------------------
-section ConditionallyCompleteLattice_lemmas
+section ConditionallyCompleteLattice
 
 variable [ConditionallyCompleteLattice R] {x : β}
 
@@ -250,7 +248,7 @@ theorem BddOn.csInf_le_csSup (s : BddOn f A) (hA : A.Nonempty) : sInf (f '' A) 
   := by --
   exact _root_.csInf_le_csSup s.below' s.above' (hA.image f) -- ∎
 
-end ConditionallyCompleteLattice_lemmas
+end ConditionallyCompleteLattice
 --------------------------------------------------------------------------------
 class Bdd [LE R] (f : β → R) : Prop where
   univ' : BddOn f Set.univ