subtypeDomain_finsupp_sum — Mathlib

English

For a finsupp-valued family with a subtype domain, sum over the subtype equals the sum of subtype-domain applications.

Русский

Для DFinsupp-объекта сумма через подтип равна сумме через приложения подтипа.

LaTeX

$$$ (s.sum h).subtypeDomain p = s.sum (\\lambda c d. (h c d).subtypeDomain p). $$$

Lean4

theorem subtypeDomain_finsupp_sum {ι} {β : ι → Type v} {δ : γ → Type x} [DecidableEq γ] [∀ c, Zero (δ c)]
    [∀ (c) (x : δ c), Decidable (x ≠ 0)] [∀ i, AddCommMonoid (β i)] {p : ι → Prop} [DecidablePred p] {s : Π₀ c, δ c}
    {h : ∀ c, δ c → Π₀ i, β i} : (s.sum h).subtypeDomain p = s.sum fun c d => (h c d).subtypeDomain p :=
  subtypeDomain_sum

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