English
For f: ι → κ, s finite in κ, and hf decidable, and g: κ → β, we have ∏ x∈s.preimage f hf, g(f x) = ∏ x∈s with x∈range f, g(x).
Русский
Пусть f: ι → κ, s ⊆ κ, hfDec и g: κ → β. Тогда ∏_{x∈s^{-1}} g(f x) = ∏_{x∈s, x∈Im f} g(x).
LaTeX
$$$\\displaystyle \\prod_{x \\in s.\\mathrm{preimage}(f)hf} g(f x) = \\prod_{x \\in s \\text{ with } x \\in \\mathrm{range\\} f} g(x)$$$
Lean4
@[to_additive]
theorem prod_preimage' (f : ι → κ) [DecidablePred (· ∈ Set.range f)] (s : Finset κ) (hf) (g : κ → β) :
∏ x ∈ s.preimage f hf, g (f x) = ∏ x ∈ s with x ∈ Set.range f, g x := by
classical
calc
∏ x ∈ preimage s f hf, g (f x) = ∏ x ∈ image f (preimage s f hf), g x :=
Eq.symm <| prod_image <| by simpa [mem_preimage, Set.InjOn] using hf
_ = ∏ x ∈ s with x ∈ Set.range f, g x := by rw [image_preimage]
