Successors and predecessors of `fin n` #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

@[protected, instance]

def fin.succ_order {n : ℕ} :

succ_order (fin n)

Equations

fin.succ_order = succ_order.of_core (λ (i : fin (n + 1)), ite (i < fin.last n) (i + 1) i) _ _
fin.succ_order = {succ := fin.elim0 (λ (ᾰ : fin 0), fin 0), le_succ := fin.succ_order._main._proof_1, max_of_succ_le := fin.succ_order._main._proof_2, succ_le_of_lt := fin.succ_order._main._proof_3, le_of_lt_succ := fin.succ_order._main._proof_4}

source

@[simp]

theorem fin.succ_eq {n : ℕ} :

succ_order.succ = λ (a : fin (n + 1)), ite (a < fin.last n) (a + 1) a

source

@[simp]

theorem fin.succ_apply {n : ℕ} (a : fin (n + 1)) :

succ_order.succ a = ite (a < fin.last n) (a + 1) a

source

@[protected, instance]

def fin.pred_order {n : ℕ} :

pred_order (fin n)

Equations

fin.pred_order = pred_order.of_core (λ (x : fin (n + 1)), ite (x = 0) 0 (x - 1)) _ _
fin.pred_order = {pred := fin.elim0 (λ (ᾰ : fin 0), fin 0), pred_le := fin.pred_order._main._proof_1, min_of_le_pred := fin.pred_order._main._proof_2, le_pred_of_lt := fin.pred_order._main._proof_3, le_of_pred_lt := fin.pred_order._main._proof_4}

source

@[simp]

theorem fin.pred_eq {n : ℕ} :

pred_order.pred = λ (a : fin (n + 1)), ite (a = 0) 0 (a - 1)

source

@[simp]

theorem fin.pred_apply {n : ℕ} (a : fin (n + 1)) :

pred_order.pred a = ite (a = 0) 0 (a - 1)

Successors and predecessors of fin n #

Successors and predecessors of `fin n` #