English
There is an unapplied analogue of the previous result: the product over s of functions g c equals the function sending a ↦ ∏_{c ∈ s} g c a.
Русский
Существует аналог предыдущего результата: произведение по s функций g c равно функциямa ↦ ∏_{c ∈ s} g c(a).
LaTeX
$$$$ \\prod_{c \\in s} g_c = \\lambda a. \\prod_{c \\in s} g_c(a). $$$$
Lean4
/-- An 'unapplied' analogue of `Finset.prod_apply`. -/
@[to_additive /-- An 'unapplied' analogue of `Finset.sum_apply`. -/
]
theorem prod_fn {α : Type*} {M : α → Type*} {ι} [∀ a, CommMonoid (M a)] (s : Finset ι) (g : ι → ∀ a, M a) :
∏ c ∈ s, g c = fun a ↦ ∏ c ∈ s, g c a :=
funext fun _ ↦ Finset.prod_apply _ _ _
