finsuppProd_mem — Mathlib

English

If S is a submonoid of N and for all c, f(c) ≠ 0 implies g(c, f(c)) ∈ S, then the product f.prod g lies in S.

Русский

Пусть S — подмоноид N; если для каждого c имеет место, что f(c) ≠ 0 → g(c, f(c)) ∈ S, тогда f.prod g ∈ S.

LaTeX

$$$$ \\forall c, f(c) \\neq 0 \\Rightarrow g(c, f(c)) \\in S \\quad \\Rightarrow \\ f.prod g \\in S $$$$

Lean4

@[to_additive]
theorem _root_.SubmonoidClass.finsuppProd_mem {S : Type*} [SetLike S N] [SubmonoidClass S N] (s : S) (f : α →₀ M)
    (g : α → M → N) (h : ∀ c, f c ≠ 0 → g c (f c) ∈ s) : f.prod g ∈ s :=
  prod_mem fun _i hi => h _ (Finsupp.mem_support_iff.mp hi)

Похожие утверждения