predAbove_of_lt_succ — Mathlib

English

Let p ∈ Fin n, i ∈ Fin(n+1) and h be i < succ p. Then p.predAbove i = i.castPred (Fin.ne_last_of_lt h).

Русский

Пусть p ∈ Fin(n), i ∈ Fin(n+1) и h: i < succ p. Тогда p.predAbove i = i.castPred (Fin.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 i = i.castPred \\bigl( \\operatorname{Fin.ne\\_last\\_of\\_lt} h \\bigr) $$$

Lean4

theorem predAbove_of_lt_succ (p : Fin n) (i : Fin (n + 1)) (h : i < succ p) :
    p.predAbove i = i.castPred (Fin.ne_last_of_lt h) :=
  predAbove_of_le_castSucc _ _ (le_castSucc_iff.mpr h)

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