prod_map — Mathlib

English

Let s be a finite set, e an embedding ι ↪ κ, and f: κ → M. Then the product over the image s.map(e) equals the product over s of f composed with e: ∏_{x ∈ s.map e} f x = ∏_{x ∈ s} f (e x).

Русский

Пусть s — конечное множество, e — вложение ι → κ, f: κ → M. Тогда произведение по s.map(e) равно произведению по s от функции f∘e: ∏_{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

@[to_additive (attr := simp)]
theorem prod_map (s : Finset ι) (e : ι ↪ κ) (f : κ → M) : ∏ x ∈ s.map e, f x = ∏ x ∈ s, f (e x) := by
  rw [Finset.prod, Finset.map_val, Multiset.map_map]; rfl

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