image_finset_prod — Mathlib

English

For a finite index set, the image of the finite product equals the finite product of images.

Русский

Для конечного множителя образ конечного произведения равен произведению образов.

LaTeX

$$Set.image f (Finset.prod s) = Finset.prod s (fun i => Set.image f (s i))$$

Lean4

@[to_additive]
theorem image_finset_prod (f : F) (m : Finset ι) (s : ι → Set α) : ((f : α → β) '' ∏ i ∈ m, s i) = ∏ i ∈ m, f '' s i :=
  (image_multiset_prod f _).trans <| congr_arg Multiset.prod <| Multiset.map_map _ _ _

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