Documentation

Mathlib.Data.Fin.SuccPred

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.

source
instance Fin.instSuccOrder {n : ℕ} :
SuccOrder (Fin n)
Equations
    source
    theorem Fin.orderSucc_eq {n : ℕ} :
    Order.succ = fun (i : Fin (n + 1)) => lastCases (last n) succ i
    source
    theorem Fin.orderSucc_apply {n : ℕ} (i : Fin (n + 1)) :
    Order.succ i = lastCases (last n) succ i
    source
    @[simp]
    theorem Fin.orderSucc_last (n : ℕ) :
    Order.succ (last n) = last n
    source
    @[simp]
    theorem Fin.orderSucc_castSucc {n : ℕ} (i : Fin n) :
    Order.succ i.castSucc = i.succ
    source
    @[deprecated Fin.orderSucc_eq (since := "2025-02-06")]
    theorem Fin.succ_eq {n : ℕ} :
    Order.succ = fun (i : Fin (n + 1)) => lastCases (last n) succ i

    Alias of Fin.orderSucc_eq.

    source
    @[deprecated Fin.orderSucc_apply (since := "2025-02-06")]
    theorem Fin.succ_apply {n : ℕ} (i : Fin (n + 1)) :
    Order.succ i = lastCases (last n) succ i

    Alias of Fin.orderSucc_apply.

    source
    instance Fin.instPredOrder {n : ℕ} :
    PredOrder (Fin n)
    Equations
      source
      theorem Fin.orderPred_eq {n : ℕ} :
      Order.succ = fun (i : Fin (n + 1)) => lastCases (last n) succ i
      source
      theorem Fin.orderPred_apply {n : ℕ} (i : Fin (n + 1)) :
      Order.pred i = cases 0 castSucc i
      source
      @[simp]
      theorem Fin.orderPred_zero (n : ℕ) :
      Order.pred 0 = 0
      source
      @[simp]
      theorem Fin.orderPred_succ {n : ℕ} (i : Fin n) :
      Order.pred i.succ = i.castSucc
      source
      @[deprecated Fin.orderPred_eq (since := "2025-02-06")]
      theorem Fin.pred_eq {n : ℕ} :
      Order.succ = fun (i : Fin (n + 1)) => lastCases (last n) succ i

      Alias of Fin.orderPred_eq.

      source
      @[deprecated Fin.orderPred_apply (since := "2025-02-06")]
      theorem Fin.pred_apply {n : ℕ} (i : Fin (n + 1)) :
      Order.pred i = cases 0 castSucc i

      Alias of Fin.orderPred_apply.