prod_mem_prod — Mathlib

English

Let I_i be a family of ideals indexed by a finite set s. If x_i ∈ I_i for all i ∈ s, then the product ∏_{i∈s} x_i lies in ∏_{i∈s} I_i.

Русский

Положим I_i — семейство идеалов, индексируемое конечным множеством s. Если x_i ∈ I_i для каждого i ∈ s, то ∏_{i∈s} x_i ∈ ∏_{i∈s} I_i.

LaTeX

$$$(\\forall i \\in s,\; x_i \\in I_i) \\Rightarrow \\left( \\prod_{i\\in s} x_i \\in \\prod_{i\\in s} I_i \\right)$$$

Lean4

theorem prod_mem_prod {ι : Type*} {s : Finset ι} {I : ι → Ideal R} {x : ι → R} :
    (∀ i ∈ s, x i ∈ I i) → (∏ i ∈ s, x i) ∈ ∏ i ∈ s, I i := by
  classical
  refine Finset.induction_on s ?_ ?_
  · grind [Submodule.mem_top]
  · grind [mul_mem_mul]

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