succAbove_last — Mathlib

English

Embedding Fin(n) into Fin(n+1) with a hole around last n is achieved by castSucc, and succAbove(last n) equals castSucc.

Русский

Встраивание Fin(n) в Fin(n+1) через пропуск вокруг последнего n достигается через castSucc, и succAbove(last n) равно castSucc.

LaTeX

$$$\forall n \in \mathbb{N},\ \mathrm{succAbove}(\mathrm{last}(n)) = \mathrm{castSucc}. $$$

Lean4

/-- Embedding `Fin n` into `Fin (n + 1)` with a hole around `last n` embeds by `castSucc`. -/
@[simp]
theorem succAbove_last : succAbove (last n) = castSucc := by ext; simp only [succAbove_of_castSucc_lt, castSucc_lt_last]

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