multipliable — Mathlib

English

For a finite index set s, the function f restricted to s (as a function on ↑s) is multipliable; i.e., the finite partial products converge in the same sense as the unrestricted function.

Русский

Для конечного множества индексов s функция f, ограниченная на ↑s, мультиплируема; то есть конечные частичные произведения сходятся так же, как и в общем случае.

LaTeX

$$$\text{Finset}(s)\Rightarrow \text{Multipliable } (f \circ (↑): (↑s) \to α)$$$

Lean4

@[to_additive]
protected theorem multipliable (s : Finset β) (f : β → α) : Multipliable (f ∘ (↑) : (↑s : Set β) → α) :=
  (s.hasProd f).multipliable

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