ofList_append — Mathlib

English

Converting concatenation of lists corresponds to concatenation of the corresponding streams: ofList (l ++ l') = append (ofList l) (ofList l').

Русский

Преобразование конкатенации списков в конкатенацию соответствующих потоков: ofList (l ++ l') = append (ofList l) (ofList l').

LaTeX

$$$\forall l\; l' : List \alpha, ofList (l ++ l') = append (ofList l) (ofList l')$$$

Lean4

@[simp]
theorem ofList_append (l l' : List α) : ofList (l ++ l') = append (ofList l) (ofList l') := by induction l <;> simp [*]

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