predAbove_zero_of_ne_zero — Mathlib

English

For [NeZero n] and i ∈ Fin(n+1), predAbove 0 i equals either 0 if i=0, otherwise i.pred hi where hi ∈ i ≠ 0.

Русский

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

LaTeX

$$$ \\forall n>0,\\ i \\in \\mathrm{Fin}(n+1),\\ predAbove(0,i) = \\begin{cases}0, & i=0, \\\\ i.\\pred(hi), & i\\neq 0 \\end{cases} $$$

Lean4

@[simp]
theorem predAbove_zero_of_ne_zero [NeZero n] {i : Fin (n + 1)} (hi : i ≠ 0) : predAbove 0 i = i.pred hi :=
  by
  obtain ⟨y, rfl⟩ := exists_succ_eq.2 hi
  exact predAbove_zero_succ

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