English
Let f: I → K and let S ⊆ Κ be finite, and suppose the restriction of f to f^{-1}(S) gives a bijection onto S. Then for every function g: K → β (with β a commutative monoid), we have ∏_{x ∈ f^{-1}(S)} g(f(x)) = ∏_{y ∈ S} g(y).
Русский
Пусть f: I → K, S ⊆ K — конечное множество, и предположим, что ограничение f на f^{-1}(S) является биекцией на S. Тогда для любой функции g: K → β (β — коммутативный моноид) выполняется равенство ∏_{x ∈ f^{-1}(S)} g(f(x)) = ∏_{y ∈ S} g(y).
LaTeX
$$$$\\forall f: I \\to K, S \\subseteq K,\\; (f|_{f^{-1}(S)}: f^{-1}(S) \\to S) \\text{ bijective} \\Rightarrow \\forall g: K \\to \\beta:\\; \\prod_{x \\in f^{-1}(S)} g(f(x)) = \\prod_{y \\in S} g(y). $$$$
Lean4
@[to_additive]
theorem prod_preimage_of_bij (f : ι → κ) (s : Finset κ) (hf : Set.BijOn f (f ⁻¹' ↑s) ↑s) (g : κ → β) :
∏ x ∈ s.preimage f hf.injOn, g (f x) = ∏ x ∈ s, g x :=
prod_preimage _ _ hf.injOn g fun _ hs h_f ↦ (h_f <| hf.subset_range hs).elim
