cons — Mathlib

English

Prepend a new element a not in the range of x to obtain an injective embedding Fin (n+1) → α.

Русский

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

LaTeX

$$$\text{cons}(x,a,h a) : \mathrm{Fin}(n+1) \hookrightarrow \alpha$$$

Lean4

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

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