append — Mathlib

English

Append of two Sym terms yields a new Sym term whose underlying multiset is the sum of the two multisets and whose length is the sum of the lengths.

Русский

Объединение двух Sym-термов даёт новый Sym-терм с суммой мультисетов и суммой длин.

LaTeX

$$$\\mathrm{append}(s,s') = \\langle s.1 + s'.1, \\; \\text{proof }\\rceil \\rangle$$$

Lean4

/-- Append a pair of `Sym` terms. -/
def append (s : Sym α n) (s' : Sym α n') : Sym α (n + n') :=
  ⟨s.1 + s'.1, by rw [Multiset.card_add, s.2, s'.2]⟩

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