feat: port Order.Cover (#1200)

leanprover-community · Dec 26, 2022 · 26b1d76 · 26b1d76
1 parent 74306d8
commit 26b1d76
Show file tree

Hide file tree

Showing 2 changed files with 553 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -399,6 +399,7 @@ import Mathlib.Order.CompleteBooleanAlgebra
 import Mathlib.Order.CompleteLattice
 import Mathlib.Order.ConditionallyCompleteLattice.Basic
 import Mathlib.Order.Copy
+import Mathlib.Order.Cover
 import Mathlib.Order.Directed
 import Mathlib.Order.Disjoint
 import Mathlib.Order.FixedPoints