succAbove_ne_last_last — Mathlib

English

Let n be a natural number and a an element of Fin(n+2) with a not equal to the last element of Fin(n+1). Then a.succAbove(last n) = last (n+1).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem succAbove_ne_last_last {a : Fin (n + 2)} (h : a ≠ last (n + 1)) : a.succAbove (last n) = last (n + 1) := by
  rw [succAbove_of_lt_succ _ _ (succ_last _ ▸ lt_last_iff_ne_last.2 h), succ_last]

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