cons_append — Mathlib

English

Appending a stream after a head element distributes with the head element: append (cons a s) t = cons a (append s t).

Русский

Добавление элемента в голову и последующее объединение распределяется над конкатенацией: append (cons a s) t = cons a (append s t).

LaTeX

$$$\forall a\, s\, t,\; append (cons a s) t = cons a (append s t)$$$

Lean4

@[simp]
theorem cons_append (a : α) (s t) : append (cons a s) t = cons a (append s t) :=
  destruct_eq_cons <| by
    dsimp [append]; rw [corec_eq]
    dsimp [append]; rw [destruct_cons]

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