feat(Data/Fin/OrderHom): Factor out succAbove and predAbove from …

…`Data.Fin.Basic`. (#10166) Move `succAbove` and `predAbove` to their own file, updating their documentation and adding an `OrderHom` instance for `predAbove`, `predAboveOrderHom`.
leanprover-community · Feb 7, 2024 · 8d817bb · 8d817bb
1 parent 031453e
commit 8d817bb
Show file tree

Hide file tree

Showing 5 changed files with 558 additions and 530 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1534,6 +1534,7 @@ import Mathlib.Data.Fin.Basic
 import Mathlib.Data.Fin.Fin2
 import Mathlib.Data.Fin.FlagRange
 import Mathlib.Data.Fin.Interval
+import Mathlib.Data.Fin.OrderHom
 import Mathlib.Data.Fin.SuccPred
 import Mathlib.Data.Fin.Tuple.Basic
 import Mathlib.Data.Fin.Tuple.BubbleSortInduction