list_prod_mem — Mathlib

English

If every element of a finite list lies in S, then the product of the elements of that list lies in S.

Русский

Если каждый элемент конечного списка принадлежит S, то произведение элементов списка принадлежит S.

LaTeX

$$$$ \\forall L:\\\\text{List}(A),\\ (\\forall x\\in L,\\ x\\in S)\\ \\Rightarrow\\ L.prod\\in S $$$$

Lean4

protected theorem list_prod_mem {L : List A} (h : ∀ x ∈ L, x ∈ S) : L.prod ∈ S :=
  list_prod_mem h

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