ofFun_prod — Mathlib

English

Let β be a CommMonoid and f: ι → α → β. Then the map ofFun 𝔖 respects finite products: ofFun 𝔖 (∏ i ∈ I, f i) = ∏ i ∈ I, ofFun 𝔖 (f i).

Русский

Пусть β — коммод-моноид; для функций f i, отображение ofFun 𝔖 сохраняет произведение над конечным числом индексов: ofFun 𝔖 (∏ i ∈ I, f i) = ∏ i ∈ I, ofFun 𝔖 (f i).

LaTeX

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

Lean4

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

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