succAbove_zero — Mathlib · SciLib

English

For the pivot zero, succAbove is the standard successor embedding: succAbove 0 equals Fin.succ.

Русский

Для нуля в качестве опорного элемента, succAbove задаёт стандартное вложение следующего элемента: succAbove 0 = Fin.succ.

LaTeX

$$$\mathrm{succAbove} \ 0 = \mathrm{Fin}.\mathrm{succ}$$$

Lean4

/-- Embedding `Fin n` into `Fin (n + 1)` with a hole around zero embeds by `succ`. -/
@[simp]
theorem succAbove_zero : succAbove (0 : Fin (n + 1)) = Fin.succ :=
  rfl

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