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.

instance Fin.instSuccOrder {n : } :
Equations
@[simp]
theorem Fin.succ_eq {n : } :
SuccOrder.succ = fun (a : Fin (n + 1)) => if a < Fin.last n then a + 1 else a
@[simp]
theorem Fin.succ_apply {n : } (a : Fin (n + 1)) :
SuccOrder.succ a = if a < Fin.last n then a + 1 else a
instance Fin.instPredOrder {n : } :
Equations
@[simp]
theorem Fin.pred_eq {n : } :
PredOrder.pred = fun (a : Fin (n + 1)) => if a = 0 then 0 else a - 1
@[simp]
theorem Fin.pred_apply {n : } (a : Fin (n + 1)) :
PredOrder.pred a = if a = 0 then 0 else a - 1