feat: port Order.Interval (#3360)

Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com> Co-authored-by: Jon Eugster <eugster.jon@gmail.com>
leanprover-community · May 22, 2023 · 02858e2 · 02858e2
1 parent c6afc89
commit 02858e2
Show file tree

Hide file tree

Showing 3 changed files with 794 additions and 1 deletion.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1821,6 +1821,7 @@ import Mathlib.Order.Hom.Order
 import Mathlib.Order.Hom.Set
 import Mathlib.Order.Ideal
 import Mathlib.Order.InitialSeg
+import Mathlib.Order.Interval
 import Mathlib.Order.Iterate
 import Mathlib.Order.JordanHolder
 import Mathlib.Order.KrullDimension