prod_mem — Mathlib

English

If every f(x) with x in a finite index set lies in S, then the finite product over that index set lies in S.

Русский

Если каждая величина f(x) для x из конечного множества индексов принадлежит S, то их произведение принадлежит S.

LaTeX

$$$$ \\forall ι,\\forall t:\\\\text{Finset}(ι),\\forall f: ι\\to A,\\ (\\\\forall x\\\\in t,\\ f x\\\\in S)\\\\Rightarrow\\ (\\\\prod x\\\\in t, f x)\\\\in S $$$$

Lean4

protected theorem prod_mem {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A]
    (S : Subalgebra R A) {ι : Type w} {t : Finset ι} {f : ι → A} (h : ∀ x ∈ t, f x ∈ S) : (∏ x ∈ t, f x) ∈ S :=
  prod_mem h

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