succAbove_castPred_of_le — Mathlib

English

Let p,i ∈ Fin(n+1) with p ≤ i and hi: i ≠ last n. Then succAbove(p.castPred hi) = (i.castPred hi).succ.

Русский

Пусть p,i ∈ Fin(n+1) с p ≤ i и hi: i ≠ last n. Тогда succAbove(p.castPred hi) = (i.castPred hi).succ.

LaTeX

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

Lean4

theorem succAbove_castPred_of_le (p i : Fin (n + 1)) (h : p ≤ i) (hi : i ≠ last n) :
    succAbove p (i.castPred hi) = (i.castPred hi).succ :=
  succAbove_of_le_castSucc _ _ (castSucc_castPred _ _ ▸ h)

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