English
Let L be a nontrivial summation filter and s a finite index set. If each f i is Multipliable with respect to L, then the tprod over β of the finite product over i in s of f i b equals the finite product over i in s of the tprod of f i.
Русский
Пусть L — ненулевой фильтр суммирования и s конечен. Если для каждого i ∈ s функция f i — Multipliable относительно L, то т-продукт по b от ∏_{i∈s} f_i(b) равен ∏_{i∈s} тпродукта f_i.
LaTeX
$$$[L.NeBot]\\ {f:\\gamma\\to\\alpha}\\ {s: Finset\\gamma}\\ (hf: \\forall i∈s, Multipliable (f i) L) : \\\\ \\prod'[L] b, \\prod_{i∈s} f i b = \\prod_{i∈s} \\prod'[L] b, f i b$$$
Lean4
@[to_additive]
protected theorem tprod_finsetProd [L.NeBot] {f : γ → β → α} {s : Finset γ} (hf : ∀ i ∈ s, Multipliable (f i) L) :
∏'[L] b, ∏ i ∈ s, f i b = ∏ i ∈ s, ∏'[L] b, f i b :=
(hasProd_prod fun i hi ↦ (hf i hi).hasProd).tprod_eq
