English
For a finite set s and embedding e, the map sending a function f: κ → M to the product ∏_{x ∈ s.map e} f x equals the function g ↦ ∏_{x ∈ s} g (e x). In particular, for all f, ∏_{x ∈ s.map e} f x = ∏_{x ∈ s} f (e x).
Русский
Для конечного множества s и вложения e отображение f: κ → M задающее продукт по s.map e эквивалентно функции, отправляющей f на ∑: для всех f: κ → M имеет равенство ∏_{x ∈ s.map e} f x = ∏_{x ∈ s} f (e x).
LaTeX
$$$\\prod_{x \\in s.map e} f\\,x = \\prod_{x \\in s} f (e\\,x)$$$
Lean4
/-- Variant of `prod_map` not applied to a function. -/
@[to_additive (attr := grind =)]
theorem prod_map' (s : Finset ι) (e : ι ↪ κ) : Finset.prod (s.map e) = fun (f : κ → M) => ∏ x ∈ s, f (e x) :=
by
funext f
simp
