image_finset_prod_pi — Mathlib

English

The image of a pi-type product over a Finset under a function equals the product of the images over each coordinate.

Русский

Образ типа пи-структуры произведения над Finset через функцию равен произведению образов по каждой координате.

LaTeX

$$((l : Finset ι) : Set ι).pi S image = ∏ i ∈ l, S i$$

Lean4

/-- The n-ary version of `Set.image_mul_prod`. -/
@[to_additive /-- The n-ary version of `Set.add_image_prod`. -/
    ]
theorem image_finset_prod_pi (l : Finset ι) (S : ι → Set α) :
    (fun f : ι → α => ∏ i ∈ l, f i) '' (l : Set ι).pi S = ∏ i ∈ l, S i :=
  by
  ext
  simp_rw [mem_finset_prod, mem_image, mem_pi, exists_prop, Finset.mem_coe]

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