succAbove_castPred_self — Mathlib

English

For p ∈ Fin(n+1) with h: p ≠ last n, succAbove p (p.castPred h) = (p.castPred h).succ.

Русский

Для p ∈ Fin(n+1) с h: p ≠ last n, succAbove p (p.castPred h) = (p.castPred h).succ.

LaTeX

$$$\forall n \in \mathbb{N},\ \forall p \in \mathrm{Fin}(n+1),\ p \neq \mathrm{last}(n) \Rightarrow \mathrm{succAbove}(p, p.castPred(h)) = (p.castPred(h)).succ.$$$

Lean4

theorem succAbove_castPred_self (p : Fin (n + 1)) (h : p ≠ last n) : succAbove p (p.castPred h) = (p.castPred h).succ :=
  succAbove_castPred_of_le _ _ Fin.le_rfl h

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