succ_ne_last_iff — Mathlib

English

For any n and any a in Fin(n+1), the successor of a is not the last element of Fin(n+1) if and only if a is not the last element of Fin(n).

Русский

Для любого n и элемента a ∈ Fin(n+1) исполнение succ(a) ≠ last(n+1) эквивалентно a ≠ last(n).

LaTeX

$$$$ \\forall n \\in \\mathbb{N}, \\forall a \\in \\mathrm{Fin}(n+1): \\operatorname{succ}(a) \\neq \\operatorname{last}(n+1) \\iff a \\neq \\operatorname{last}(n). $$$$

Lean4

theorem succ_ne_last_iff (a : Fin (n + 1)) : succ a ≠ last (n + 1) ↔ a ≠ last n :=
  not_iff_not.mpr <| succ_eq_last_succ

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