imports

Author: j-loreaux

Mathlib.lean

@@ -5579,6 +5579,7 @@ public import Mathlib.Order.ConditionallyCompleteLattice.Group
 public import Mathlib.Order.ConditionallyCompleteLattice.Indexed
 public import Mathlib.Order.ConditionallyCompletePartialOrder.Basic
 public import Mathlib.Order.ConditionallyCompletePartialOrder.Defs
+public import Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
 public import Mathlib.Order.Copy
 public import Mathlib.Order.CountableDenseLinearOrder
 public import Mathlib.Order.Cover

Mathlib/Order/ConditionallyCompletePartialOrder/Basic.lean

@@ -5,10 +5,8 @@ Authors: Jireh Loreaux
 -/
 module
 
-public import Mathlib.Order.Bounds.Image
 public import Mathlib.Order.CompleteLattice.Defs
 public import Mathlib.Order.ConditionallyCompletePartialOrder.Defs
-public import Mathlib.Order.WithBot
 
 import Mathlib.Data.Set.Lattice