succAbove_of_lt_succ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem succAbove_of_lt_succ (p : Fin (n + 1)) (i : Fin n) (h : p < succ i) : p.succAbove i = succ i :=
  succAbove_of_le_castSucc _ _ (le_castSucc_iff.mpr h)

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