predAbove_succ_of_lt — Mathlib

English

For p ∈ Fin n and i ∈ Fin(n+1) with i < succ p, p.predAbove (succ i) = (i.succ).castPred (succ_ne_last_of_lt h).

Русский

Пусть p ∈ Fin(n) и i ∈ Fin(n+1) и i < succ p. Тогда p.predAbove (succ i) = (i.succ).castPred (succ_ne_last_of_lt h).

LaTeX

$$$ \\forall p \\in \\mathrm{Fin}(n), \\forall i \\in \\mathrm{Fin}(n+1),\\ h:\\ i < \\operatorname{succ}(p) \\\\ :\\ p.predAbove(\\operatorname{succ}(i)) = (\\operatorname{succ}(i)).castPred(\\operatorname{succ\\_ne\\_last\\_of\\_lt} h) $$$

Lean4

theorem predAbove_succ_of_lt (p i : Fin n) (h : i < p) :
    p.predAbove (succ i) = (i.succ).castPred (succ_ne_last_of_lt h) := by
  rw [predAbove_of_lt_succ _ _ (succ_lt_succ_iff.mpr h)]

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