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 : ℕ} : SuccOrder (Fin n)

Equations

• One or more equations did not get rendered due to their size.

@[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 : ℕ} : PredOrder (Fin n)

Equations

• One or more equations did not get rendered due to their size.

@[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