lift_ofList — Mathlib

English

For any function f: α → M and any list l of elements of α, lift f applied to the word ofList l equals the product in M of f applied pointwise to the elements of l, i.e., lift f (ofList l) = (l.map f).prod.

Русский

Для любой функции f: α → M и любого списка l, применение lift к слову ofList l равно произведению в M значений f на элементах списка: lift f (ofList l) = (l.map f).prod.

LaTeX

$$$ lift\ f\ (ofList\ l) = (l.map\ f)\ .prod $$$

Lean4

@[to_additive (attr := simp)]
theorem lift_ofList (f : α → M) (l : List α) : lift f (ofList l) = (l.map f).prod :=
  prodAux_eq _

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