ofStream_append — Mathlib

English

Embedding a concatenation of a list and a stream equals the concatenation of the embeddings: ofStream (l ++ₛ s) = append (ofList l) (ofStream s).

Русский

Встраивание конкатенации списка и потока равно конкатенации их встроек: ofStream (l ++ₛ s) = append (ofList l) (ofStream s).

LaTeX

$$$\forall {l : List \alpha} {s : Stream' \alpha},\; ofStream (l ++ₛ s) = append (ofList l) (ofStream s)$$$

Lean4

@[simp]
theorem ofStream_append (l : List α) (s : Stream' α) : ofStream (l ++ₛ s) = append (ofList l) (ofStream s) := by
  induction l <;> simp [*, Stream'.nil_append_stream, Stream'.cons_append_stream]

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