# Documentation

Mathlib.Data.Fin.SuccPred

# Successors and predecessors of Fin n#

In this file, we show that Fin n is both a SuccOrder and a PredOrder. Note that they are also archimedean, but this is derived from the general instance for well-orderings as opposed to a specific Fin instance.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Fin.succ_eq {n : } :
SuccOrder.succ = fun a => if a < then a + 1 else a
@[simp]
theorem Fin.succ_apply {n : } (a : Fin (n + 1)) :
= if a < then a + 1 else a
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Fin.pred_eq {n : } :
PredOrder.pred = fun a => if a = 0 then 0 else a - 1
@[simp]
theorem Fin.pred_apply {n : } (a : Fin (n + 1)) :
= if a = 0 then 0 else a - 1