succAbove_castPred_of_lt — Mathlib

English

If i < p for p,i ∈ Fin(n+1), then p.castPred(hi).succAbove(i.castPred) = i.castPred.

Русский

Если i < p для p,i ∈ Fin(n+1), то p.castPred(hi).succAbove(i.castPred) = i.castPred.

LaTeX

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

Lean4

theorem succAbove_castPred_of_lt (p i : Fin (n + 1)) (h : i < p) :
    succAbove p (i.castPred (Fin.ne_of_lt <| Nat.lt_of_lt_of_le h p.le_last)) = i := by
  rw [succAbove_of_castSucc_lt _ _ (castSucc_castPred _ _ ▸ h), castSucc_castPred]

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