append_assoc

Mathlib.Data.WSeq.Basic

URI: https://scilib.ai/kg/mathlib#Stream'.WSeq.append_assoc

English

append is associative: append(append s t) u = append s (append t u).

Русский

Сложение является ассоциативным: (append(append(s,t), u) = append(s, append(t,u))).

LaTeX

$$$$\operatorname{append}(\operatorname{append}(s,t), u) = \operatorname{append}(s, \operatorname{append}(t,u)).$$$$

Lean4

@[simp]
theorem append_assoc (s t u : WSeq α) : append (append s t) u = append s (append t u) :=
  Seq.append_assoc _ _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru