English
Append two compositions to obtain a composition whose blocks are the concatenation of the blocks of the two inputs; total sum is the sum of the sums.
Русский
Соединение двух композиции даёт композицию, чьи блоки образуют конкатенацию блоков входных композиций; сумма блоков равна сумме их сумм.
LaTeX
$$$\\mathrm{append}:\\mathrm{Composition}(m) \\to \\mathrm{Composition}(n) \\to \\mathrm{Composition}(m+n),\\ \\text{blocks} = \\mathrm{blocks}(c_1) \\cup \\mathrm{blocks}(c_2),\\ \\mathrm{blocks\\_sum} = \\mathrm{blocks\\_sum}(c_1) + \\mathrm{blocks\\_sum}(c_2).$$$
Lean4
/-- Append two compositions to get a composition of the sum of numbers. -/
@[simps]
def append (c₁ : Composition m) (c₂ : Composition n) : Composition (m + n)
where
blocks := c₁.blocks ++ c₂.blocks
blocks_pos := by
intro i hi
rw [mem_append] at hi
exact hi.elim c₁.blocks_pos c₂.blocks_pos
blocks_sum := by simp
