succAbove_of_succ_le — Mathlib

English

Let p ∈ Fin(n+1) and i ∈ Fin(n). If succ(i) ≤ p, then p.succAbove(i) = castSucc(i).

Русский

Пусть p ∈ Fin(n+1) и i ∈ Fin(n). Если succ(i) ≤ p, тогда p.succAbove(i) = castSucc(i).

LaTeX

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

Lean4

theorem succAbove_of_succ_le (p : Fin (n + 1)) (i : Fin n) (h : succ i ≤ p) : p.succAbove i = castSucc i :=
  succAbove_of_castSucc_lt _ _ (castSucc_lt_iff_succ_le.mpr h)

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