English
If g is injective on s, then the product over g''s equals the product of f(g i) over i ∈ s: ∏_{i∈g''s} f(i) = ∏_{i∈s} f(g(i)).
Русский
Если отображение g инъективно на s, то произведение по образу совпадает с произведением по композиции: ∏_{y ∈ g''s} f(y) = ∏_{x ∈ s} f(g(x)).
LaTeX
$$\operatorname{Injective}(g|_{s}) \Rightarrow \prod_{i \in g'' s} f(i) = \prod_{j \in s} f(g(j))$$
Lean4
/-- The product of `f y` over `y ∈ g '' s` equals the product of `f (g i)` over `s` provided that
`g` is injective on `s`. -/
@[to_additive /-- The sum of `f y` over `y ∈ g '' s` equals the sum of `f (g i)` over `s` provided that
`g` is injective on `s`. -/
]
theorem finprod_mem_image {s : Set β} {g : β → α} (hg : s.InjOn g) : ∏ᶠ i ∈ g '' s, f i = ∏ᶠ j ∈ s, f (g j) :=
finprod_mem_image' <| hg.mono inter_subset_left
