predAbove_last_of_ne_last — Mathlib

English

For n, i ∈ Fin(n+2) with i ≠ last(n+1), predAbove (last n) i = castPred i hi.

Русский

Для n, i ∈ Fin(n+2) при i ≠ last(n+1) выполняется predAbove (last n) i = castPred i hi.

LaTeX

$$$ \\forall n, i \\in \\mathrm{Fin}(n+2),\\ hi:\\ i \\neq \\operatorname{last}(n+1) \\\\ :\\ \\operatorname{predAbove}(\\operatorname{last} n, i) = i.castPred~hi $$$

Lean4

@[simp]
theorem predAbove_last_of_ne_last {i : Fin (n + 2)} (hi : i ≠ last (n + 1)) : predAbove (last n) i = castPred i hi :=
  by
  rw [← exists_castSucc_eq] at hi
  rcases hi with ⟨y, rfl⟩
  exact predAbove_last_castSucc

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