succAbove_pred_of_le — Mathlib

English

If i ≤ p in Fin(n+1) with i ≠ 0, then p.succAbove(i.pred(hi)) = (i.pred(hi)).castSucc.

Русский

Если i ≤ p в Fin(n+1) и i ≠ 0, то p.succAbove(i.pred(hi)) = (i.pred(hi)).castSucc.

LaTeX

$$$\forall n \in \mathbb{N},\ \forall p,i\in \mathrm{Fin}(n+1),\ i \le p \Rightarrow \exists hi:\mathrm{Pred}(i,hi) :\ succAbove(p, i.pred(hi)) = (i.pred(hi)).castSucc. $$$

Lean4

theorem succAbove_pred_of_le (p i : Fin (n + 1)) (h : i ≤ p) (hi : i ≠ 0) :
    succAbove p (i.pred hi) = (i.pred hi).castSucc :=
  succAbove_of_succ_le _ _ (succ_pred _ _ ▸ h)

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