dfinsuppSum_mem — Mathlib

English

If S is a submodule and f is a dependent finite-support family, then the dfinsupp sum f g lies in S provided g respects S entrywise.

Русский

Если S — подмодуль, а f — зависимая сумма с конечной поддержкой, то dfinsuppSum f g ∈ S при условии, что g(i, f(i)) ∈ S для каждого i.

LaTeX

$$$f.sum g ∈ S$ under the given hypotheses$$

Lean4

theorem dfinsuppSum_mem {β : ι → Type*} [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] (S : Submodule R N)
    (f : Π₀ i, β i) (g : ∀ i, β i → N) (h : ∀ c, f c ≠ 0 → g c (f c) ∈ S) : f.sum g ∈ S :=
  _root_.dfinsuppSum_mem S f g h

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