succAbove_ne_last — Mathlib

English

If a ∈ Fin(n+2) and b ∈ Fin(n+1) are both not equal to the last element of their respective types, then a.succAbove(b) ≠ last(n+1).

Русский

Если a ∈ Fin(n+2) и b ∈ Fin(n+1) не равны своим последним элементам, то a.succAbove(b) ≠ last(n+1).

LaTeX

$$$\forall n \in \mathbb{N}\, \forall a \in \mathrm{Fin}(n+2)\, \forall b \in \mathrm{Fin}(n+1),\ a \neq \mathrm{last}(n+1)\ \land\ b \neq \mathrm{last}(n)\Rightarrow a\.succAbove(b) \neq \mathrm{last}(n+1).$$$

Lean4

theorem succAbove_ne_last {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a ≠ last _) (hb : b ≠ last _) :
    a.succAbove b ≠ last _ :=
  mt (succAbove_eq_last_iff ha).mp hb

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