init — Mathlib

English

Remove the last element of an injective (n+1)-tuple to obtain an injective Fin n → α embedding.

Русский

Удаление последнего элемента у инъективной кортежной функции (n+1) элементов даёт инъекцию Fin n → α.

LaTeX

$$$\text{init}: \mathrm{Fin}(n+1) \hookrightarrow \alpha \to \mathrm{Fin}n \hookrightarrow \alpha$$$

Lean4

/-- Remove the last element from an injective (n + 1)-tuple. -/
def init {n : ℕ} (x : Fin (n + 1) ↪ α) : Fin n ↪ α :=
  ⟨Fin.init x, x.injective.comp <| castSucc_injective _⟩

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