succAbove_pred_of_lt — Mathlib

English

Given p,i ∈ Fin(n+1) with p < i, then p.succAbove(i.pred(h)) = i, where h certifies the predecessor exists.

Русский

Для p,i ∈ Fin(n+1) при p < i выполняется p.succAbove(i.pred(h)) = i, где h гарантирует существование предшественника.

LaTeX

$$$\forall n \in \mathbb{N},\ \forall p,i \in \mathrm{Fin}(n+1),\ p < i \Rightarrow \mathrm{succAbove}(p, i.pred(h)) = i,$ where $h$ is the appropriate witness. $$$

Lean4

theorem succAbove_pred_of_lt (p i : Fin (n + 1)) (h : p < i) :
    succAbove p (i.pred (Fin.ne_of_gt <| Fin.lt_of_le_of_lt p.zero_le h)) = i := by
  rw [succAbove_of_lt_succ _ _ (succ_pred _ _ ▸ h), succ_pred]

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