# mathlibdocumentation

data.fin.succ_pred

# Successors and predecessors of fin n#

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

@[protected, instance]
def fin.succ_order {n : } :
Equations
@[simp]
theorem fin.succ_eq {n : } :
succ_order.succ = λ (a : fin (n + 1)), ite (a < fin.last n) (a + 1) a
@[simp]
theorem fin.succ_apply {n : } (a : fin (n + 1)) :
= ite (a < fin.last n) (a + 1) a
@[protected, instance]
def fin.pred_order {n : } :
Equations
@[simp]
theorem fin.pred_eq {n : } :
pred_order.pred = λ (a : fin (n + 1)), ite (a = 0) 0 (a - 1)
@[simp]
theorem fin.pred_apply {n : } (a : fin (n + 1)) :
= ite (a = 0) 0 (a - 1)