feat: port Order.Bounds.Basic (#1040)

aba57d4d3dae35460225919dcd82fe91355162f9 Co-authored-by: Winston Yin <winstonyin@gmail.com> Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
leanprover-community · Dec 15, 2022 · c455292 · c455292
1 parent 1305c79
commit c455292
Show file tree

Hide file tree

Showing 2 changed files with 1,626 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -311,6 +311,7 @@ import Mathlib.Order.Antisymmetrization
 import Mathlib.Order.Basic
 import Mathlib.Order.BooleanAlgebra
 import Mathlib.Order.BoundedOrder
+import Mathlib.Order.Bounds.Basic
 import Mathlib.Order.Compare
 import Mathlib.Order.Directed
 import Mathlib.Order.Disjoint