predAbove_right_last — Mathlib

English

For i ∈ Fin(n) and any i, predAbove(i, last(n+1)) = last n.

Русский

Для i ∈ Fin(n) и произвольного last(n+1) predAbove(i, last(n+1)) = last n.

LaTeX

$$$ \\forall i \\in \\mathrm{Fin}(n),\\ \\operatorname{predAbove}(i,\\operatorname{last}(n+1)) = \\operatorname{last} n $$$

Lean4

@[simp]
theorem predAbove_right_last {i : Fin (n + 1)} : predAbove i (last (n + 1)) = last n := by
  rw [predAbove_of_castSucc_lt _ _ (castSucc_lt_last _), pred_last]

Похожие утверждения