English
Let s be a finite index set and f: ι → C(α, β) a family of continuous maps into a topological monoid β with continuous multiplication. The product of maps ∏ i∈s f(i) corresponds to the function a ↦ ∏ i∈s f(i)(a). In particular, the evaluation of the finite product map equals the finite product of evaluations.
Русский
Пусть s — конечный индексный набор, и дана семья непрерывных отображений f(i): α → β. Тогда произведение функций ∏_{i∈s} f(i) соответствует функции a ↦ ∏_{i∈s} f(i)(a). В частности, значение конечного произведения равно произведению значений на каждом аргументе.
LaTeX
$$$\big(\prod_{i \in s} f(i)\big)(a) = \prod_{i \in s} (f(i)(a))$, для всех $a \in α$.$$
Lean4
@[to_additive (attr := simp)]
theorem coe_prod [CommMonoid β] [ContinuousMul β] {ι : Type*} (s : Finset ι) (f : ι → C(α, β)) :
⇑(∏ i ∈ s, f i) = ∏ i ∈ s, (f i : α → β) :=
map_prod coeFnMonoidHom f s
