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

• Fin.instSuccOrder = { succ := fun (a : Fin 0) => a.elim0, le_succ := Fin.instSuccOrder.proof_1, max_of_succ_le := @Fin.instSuccOrder.proof_2, succ_le_of_lt := @Fin.instSuccOrder.proof_3 }
• Fin.instSuccOrder = SuccOrder.ofCore (fun (i : Fin (n + 1)) => if i < Fin.last n then i + 1 else i) ⋯ ⋯

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

• Fin.instPredOrder = { pred := fun (a : Fin 0) => a.elim0, pred_le := Fin.instPredOrder.proof_1, min_of_le_pred := @Fin.instPredOrder.proof_2, le_pred_of_lt := @Fin.instPredOrder.proof_3 }
• Fin.instPredOrder = PredOrder.ofCore (fun (x : Fin (n + 1)) => if x = 0 then 0 else x - 1) ⋯ ⋯

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