predAbove_castSucc_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 \\\\ :\\ p.predAbove(\\operatorname{castSucc}(i)) = i.castSucc.pred(\\operatorname{castSucc\\_ne\\_zero\\_of\\_lt} h) $$$

Lean4

theorem predAbove_castSucc_of_lt (p i : Fin n) (h : p < i) :
    p.predAbove (castSucc i) = i.castSucc.pred (castSucc_ne_zero_of_lt h) := by
  rw [predAbove_of_castSucc_lt _ _ (castSucc_lt_castSucc_iff.2 h)]

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