predAbove_castPred_self — Mathlib

English

For p ∈ Fin(n+1) and hp ≠ last n, (castPred p hp).predAbove p = p.castPred hp.

Русский

Для p ∈ Fin(n+1) и hp ≠ last n: (castPred p hp).predAbove p = p.castPred hp.

LaTeX

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

Lean4

theorem predAbove_castPred_self (p : Fin (n + 1)) (hp : p ≠ last n) : (castPred p hp).predAbove p = castPred p hp :=
  predAbove_castPred_of_le _ _ Fin.le_rfl hp

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