list_prod_mem_list_prod — Mathlib

English

If each g(i) ∈ f(i) for i in a list, then the product of the g(i) lies in the product of the f(i).

Русский

Если для каждого элемента списка выполняется g(i) ∈ f(i), то произведение g(i) лежит в произведении f(i).

LaTeX

$$(t.map g).prod ∈ (t.map f).prod$$

Lean4

/-- An n-ary version of `Set.mul_mem_mul`. -/
@[to_additive /-- An n-ary version of `Set.add_mem_add`. -/
    ]
theorem list_prod_mem_list_prod (t : List ι) (f : ι → Set α) (g : ι → α) (hg : ∀ i ∈ t, g i ∈ f i) :
    (t.map g).prod ∈ (t.map f).prod := by
  induction t with
  | nil => simp_rw [List.map_nil, List.prod_nil, Set.mem_one]
  | cons h tl ih =>
    simp_rw [List.map_cons, List.prod_cons]
    exact mul_mem_mul (hg h List.mem_cons_self) (ih fun i hi ↦ hg i <| List.mem_cons_of_mem _ hi)

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