append_nil

Mathlib.Data.WSeq.Basic

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

English

append s nil = s.

Русский

Сложение s и nil даёт s.

LaTeX

$$$$\operatorname{append}(s, \mathrm{nil}) = s.$$$$

Lean4

@[simp]
theorem append_nil (s : WSeq α) : append s nil = s :=
  Seq.append_nil _

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

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

Разделы

Аффилиация

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