ofList_append — Mathlib

English

The image of concatenation under ofList is the product of images: ofList (xs ++ ys) = ofList xs * ofList ys.

Русский

Образ конкатенации под действием ofList равен произведению образов: ofList (xs ++ ys) = ofList xs * ofList ys.

LaTeX

$$$ ofList (xs ++ ys) = ofList xs * ofList ys $$$

Lean4

@[to_additive (attr := simp)]
theorem ofList_append (xs ys : List α) : ofList (xs ++ ys) = ofList xs * ofList ys :=
  rfl

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