toFun_prod — Mathlib

English

For β a CommMonoid and f: ι → α → β, the evaluation map preserves finite products: toFun 𝔖 (∏ i ∈ I, f i) = ∏ i ∈ I, toFun 𝔖 (f i).

Русский

Для β, являющегося комм. моноидом, и функций f i, сопоставление toFun сохраняет произведение: toFun 𝔖 (∏ i ∈ I, f i) = ∏ i ∈ I, toFun 𝔖 (f i).

LaTeX

$$$\mathrm{toFun}_{\mathfrak{S}}\left(\prod_{i \in I} f_i\right) = \prod_{i \in I} \mathrm{toFun}_{\mathfrak{S}}(f_i).$$$

Lean4

@[to_additive (attr := simp)]
theorem toFun_prod {β : Type*} [CommMonoid β] {f : ι → α → β} (I : Finset ι) :
    toFun (∏ i ∈ I, f i) = ∏ i ∈ I, toFun (f i) :=
  rfl

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