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.

ink

instance Fin.instForAllNatSuccOrderFinToPreorderInstPartialOrderFin {n : ℕ} : SuccOrder (Fin n)

Equations

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

ink

@[simp]

theorem Fin.succ_eq {n : ℕ} : SuccOrder.succ = fun a => if a < Fin.last n then a + 1 else a

ink

@[simp]

theorem Fin.succ_apply {n : ℕ} (a : Fin (n + 1)) : SuccOrder.succ a = if a < Fin.last n then a + 1 else a

ink

instance Fin.instForAllNatPredOrderFinToPreorderInstPartialOrderFin {n : ℕ} : PredOrder (Fin n)

Equations

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

ink

@[simp]

theorem Fin.pred_eq {n : ℕ} : PredOrder.pred = fun a => if a = 0 then 0 else a - 1

ink

@[simp]

theorem Fin.pred_apply {n : ℕ} (a : Fin (n + 1)) : PredOrder.pred a = if a = 0 then 0 else a - 1