feat: port Order.SuccPred.Basic (#1233)

Port of order.succ_pred.basic
leanprover-community · Jan 1, 2023 · a6184c4 · a6184c4
1 parent 25a1365
commit a6184c4
Show file tree

Hide file tree

Showing 3 changed files with 1,498 additions and 1 deletion.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -455,6 +455,7 @@ import Mathlib.Order.RelIso.Basic
 import Mathlib.Order.RelIso.Group
 import Mathlib.Order.RelIso.Set
 import Mathlib.Order.SemiconjSup
+import Mathlib.Order.SuccPred.Basic
 import Mathlib.Order.SymmDiff
 import Mathlib.Order.Synonym
 import Mathlib.Order.WellFounded

diff --git a/Mathlib/Order/RelClasses.lean b/Mathlib/Order/RelClasses.lean
@@ -408,7 +408,7 @@ def toWellFoundedRelation : WellFoundedRelation α :=
 end WellFoundedGt
 
 /-- Construct a decidable linear order from a well-founded linear order. -/
-noncomputable def IsWellOrder.LinearOrder (r : α → α → Prop) [IsWellOrder α r] : LinearOrder α :=
+noncomputable def IsWellOrder.linearOrder (r : α → α → Prop) [IsWellOrder α r] : LinearOrder α :=
   letI := fun x y => Classical.dec ¬r x y
   linearOrderOfSTO r