predAbove_castPred_of_lt — Mathlib

English

If p < i for p,i ∈ Fin n, then (p.predAbove (castSucc i)) = i.castSucc.pred (castSucc_ne_zero_of_lt h).

Русский

Если p < i для p,i ∈ Fin n, то (p.predAbove (castSucc i)) = i.castSucc.pred (castSucc_ne_zero_of_lt h).

LaTeX

$$$ \\forall p,i \\in \\mathrm{Fin}(n),\\ h:\\ p < i \\\\ :\\ (\\operatorname{predAbove}~p~(\\operatorname{castSucc}(i))).predAbove = i.castSucc.pred(\\operatorname{castSucc\\_ne\\_zero\\_of\\_lt} h) $$$

Lean4

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

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