English
Given a family of submonoids S_i and a dfinsupp f with coefficients in β_i, if g_i maps f_i into γ from β_i and h ensures the image lies in S_i for nonzero f_i, then f.prod g ∈ S.
Русский
При данных подмножеств S_i и dfinsupp f с коэффициентами в β_i, если g_i(f_i) попадает в S_i для каждого i, и это сохраняется для ненулевых координат, то f.prod g принадлежит произведению.
LaTeX
$$$ f.prod g \in S $ под условием выше$$
Lean4
@[to_additive]
theorem dfinsuppProd_mem [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ] {S : Type*} [SetLike S γ]
[SubmonoidClass S γ] (s : S) (f : Π₀ i, β i) (g : ∀ i, β i → γ) (h : ∀ c, f c ≠ 0 → g c (f c) ∈ s) : f.prod g ∈ s :=
prod_mem fun _ hi => h _ <| mem_support_iff.1 hi
