predAbove_pred_of_lt — Mathlib

English

Let p,i ∈ Fin(n+1) with i < p. Then (pred p (Fin.ne_zero_of_lt h)).predAbove i = castPred i (Fin.ne_last_of_lt h).

Русский

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

LaTeX

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

Lean4

theorem predAbove_pred_of_lt (p i : Fin (n + 1)) (h : i < p) :
    (pred p (Fin.ne_zero_of_lt h)).predAbove i = castPred i (Fin.ne_last_of_lt h) := by
  rw [predAbove_of_lt_succ _ _ (succ_pred _ _ ▸ h)]

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