feat: port Order.SuccPred.LinearLocallyFinite (#2033)

leanprover-community · Feb 3, 2023 · cc3de2a · cc3de2a
1 parent d050243
commit cc3de2a
Show file tree

Hide file tree

Showing 2 changed files with 456 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -826,6 +826,7 @@ import Mathlib.Order.SemiconjSup
 import Mathlib.Order.SuccPred.Basic
 import Mathlib.Order.SuccPred.IntervalSucc
 import Mathlib.Order.SuccPred.Limit
+import Mathlib.Order.SuccPred.LinearLocallyFinite
 import Mathlib.Order.SuccPred.Relation
 import Mathlib.Order.SupIndep
 import Mathlib.Order.SymmDiff