English
Let α be an additive structure. For i and hid with i < d, and holors x, y of shape d :: ds, the i-th slice distributes over addition: slice x i hid + slice y i hid = slice (x + y) i hid.
Русский
Пусть α обладает присоединенной структурой; для i и доказательства i < d, и холоров x, y формы d :: ds выполняется дистрибутивность среза над сложением: slice x i hid + slice y i hid = slice (x + y) i hid.
LaTeX
$$$$ \\operatorname{slice} x\\ i\\ hid + \\operatorname{slice} y\\ i\\ hid = \\operatorname{slice}(x + y)\\ i\\ hid $$$$
Lean4
theorem slice_add [Add α] (i : ℕ) (hid : i < d) (x : Holor α (d :: ds)) (y : Holor α (d :: ds)) :
slice x i hid + slice y i hid = slice (x + y) i hid :=
funext fun t => by simp [slice, (· + ·), Add.add]
