eqOn_fun_finsetProd — Mathlib

English

If, for each i, f_i and f'_i are equal on a set s, then the finite product over i∈v of f_i is equal on s to the product of f'_i.

Русский

Если для каждого i возможно f_i и f'_i совпадают на множестве s, то произведение по i∈v функций f_i совпадает на s с произведением f'_i.

LaTeX

$$$$ \\forall v, \\; \\text{Set.EqOn} \\bigg( \\prod_{i\\in v} f_i \\bigg) \\bigg( \\prod_{i\\in v} f'_i \\bigg) s. $$$$

Lean4

@[to_additive]
theorem eqOn_fun_finsetProd {ι α β : Type*} [CommMonoid α] {s : Set β} {f f' : ι → β → α}
    (h : ∀ (i : ι), Set.EqOn (f i) (f' i) s) (v : Finset ι) :
    Set.EqOn (fun b ↦ ∏ i ∈ v, f i b) (fun b ↦ ∏ i ∈ v, f' i b) s := by convert eqOn_finsetProd h v <;> simp

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