SuccOrder and PredOrder 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)) => Fin.lastCases (Fin.last n) Fin.succ i) ⋯ ⋯

theorem Fin.orderSucc_eq {n : ℕ} : Order.succ = fun (i : Fin (n + 1)) => lastCases (last n) succ i

theorem Fin.orderSucc_apply {n : ℕ} (i : Fin (n + 1)) : Order.succ i = lastCases (last n) succ i

@[simp]

theorem Fin.orderSucc_last (n : ℕ) : Order.succ (last n) = last n

@[simp]

theorem Fin.orderSucc_castSucc {n : ℕ} (i : Fin n) : Order.succ i.castSucc = i.succ

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 (i : Fin (n + 1)) => Fin.cases 0 Fin.castSucc i) ⋯ ⋯

theorem Fin.orderPred_eq {n : ℕ} : Order.succ = fun (i : Fin (n + 1)) => lastCases (last n) succ i

theorem Fin.orderPred_apply {n : ℕ} (i : Fin (n + 1)) : Order.pred i = cases 0 castSucc i

@[simp]

theorem Fin.orderPred_zero (n : ℕ) : Order.pred 0 = 0

@[simp]

theorem Fin.orderPred_succ {n : ℕ} (i : Fin n) : Order.pred i.succ = i.castSucc