snoc — Mathlib

English

Append a new element a to an injective n-tuple to obtain an injective n+1-tuple Fin (n+1) → α.

Русский

Добавляем новый элемент a к инъективному n-кортежу, получая инъекцию Fin(n+1) → α.

LaTeX

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

Lean4

/-- Adding a new element at the end of an injective n-tuple, to get an injective n+1-tuple. -/
def snoc {n : ℕ} (x : Fin n ↪ α) {a : α} (ha : a ∉ range x) : Fin (n + 1) ↪ α :=
  ⟨Fin.snoc x a, snoc_injective_iff.mpr ⟨x.inj', ha⟩⟩

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