English
A further generalization: for f and finite disjoint s,t with a certain disjointness condition on mulSupport f, we have ∏_{i∈s∪t} f(i) = (∏_{i∈s} f(i)) (∏_{i∈t} f(i)).
Русский
Ещё одна обобщение: для f и конечных непересекающихся s,t с условием на mulSupport f выполняется ∏_{i∈s∪t} f(i) = (∏_{i∈s} f(i)) (∏_{i∈t} f(i)).
LaTeX
$$(hst : Disjoint (s ∩ mulSupport f) (t ∩ mulSupport f)) → (hs : (s ∩ mulSupport f).Finite) → (ht : (t ∩ mulSupport f).Finite) → ∏ᶠ i ∈ s ∪ t, f i = (∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ t, f i$$
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 ∩ mulSupport (f ∘ g)`. -/
@[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 ∩ support (f ∘ g)`. -/
]
theorem finprod_mem_image' {s : Set β} {g : β → α} (hg : (s ∩ mulSupport (f ∘ g)).InjOn g) :
∏ᶠ i ∈ g '' s, f i = ∏ᶠ j ∈ s, f (g j) := by
classical
by_cases hs : (s ∩ mulSupport (f ∘ g)).Finite
· have hg : ∀ x ∈ hs.toFinset, ∀ y ∈ hs.toFinset, g x = g y → x = y := by simpa only [hs.mem_toFinset]
have := finprod_mem_eq_prod (comp f g) hs
unfold Function.comp at this
rw [this, ← Finset.prod_image hg]
refine finprod_mem_eq_prod_of_inter_mulSupport_eq f ?_
rw [Finset.coe_image, hs.coe_toFinset, ← image_inter_mulSupport_eq, inter_assoc, inter_self]
· unfold Function.comp at hs
rw [finprod_mem_eq_one_of_infinite hs, finprod_mem_eq_one_of_infinite]
rwa [image_inter_mulSupport_eq, infinite_image_iff hg]
