predAbove_zero_succ — Mathlib

English

If [NeZero n] and i ∈ Fin(n+1) with i ≠ 0, then predAbove 0 i = i.pred hi where hi expresses i ≠ 0.

Русский

Если [NeZero n] и i ∈ Fin(n+1) и i ≠ 0, то predAbove 0 i = i.pred hi, где hi указывает, что i ≠ 0.

LaTeX

$$$ \\forall n>0,\\ \\forall i \\in \\mathrm{Fin}(n+1),\\ i \\neq 0 \\Rightarrow \\operatorname{predAbove}(0,i) = i.\\operatorname{pred}(\\text{hi}) $$$

Lean4

theorem predAbove_zero_succ [NeZero n] {i : Fin n} : predAbove 0 i.succ = i := by
  rw [predAbove_succ_of_le _ _ (Fin.zero_le _)]

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