succAbove_eq_last_iff — Mathlib

English

Let a ∈ Fin(n+2), b ∈ Fin(n+1) with a ≠ last(n+1). Then a.succAbove(b) = last(n+1) if and only if b = last(n).

Русский

Пусть a ∈ Fin(n+2), b ∈ Fin(n+1) и a ≠ last(n+1). Тогда a.succAbove(b) = last(n+1) эквивалентно b = last(n).

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) \Rightarrow\bigl(a\.succAbove(b) = \mathrm{last}(n+1) \iff b = \mathrm{last}(n)\bigr).$$$

Lean4

theorem succAbove_eq_last_iff {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a ≠ last _) :
    a.succAbove b = last _ ↔ b = last _ := by rw [← succAbove_ne_last_last ha, succAbove_right_inj]

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