cons — Mathlib

English

Inserting an element a into s increases the length by one; the underlying multiset becomes a ::ₘ s.

Русский

Вставка элемента a в s увеличивает длину на единицу; мультисет становится a ::ₘ s.

LaTeX

$$$ (a ::_\mathrm{s} \; : \mathrm{Multiset}(\alpha)) = a ::_m (s : \mathrm{Multiset}(\alpha)) $$$

Lean4

/-- Inserts an element into the term of `Sym α n`, increasing the length by one.
-/
@[match_pattern]
def cons (a : α) (s : Sym α n) : Sym α n.succ :=
  ⟨a ::ₘ s.1, by rw [Multiset.card_cons, s.2]⟩

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