subtypeDomain_sum — Mathlib

English

Distributes over finite sums: subtypeDomain commutes with Finset sum.

Русский

Распространяется на конечные суммы: subtypeDomain коммутирует с суммой по множителям.

LaTeX

$$$ \\text{subtypeDomain } p \\Bigl( \\sum_{c \\in s} h(c) \\Bigr) = \\sum_{c \\in s} \\text{subtypeDomain } p \\bigl( h(c) \\bigr). $$$

Lean4

theorem subtypeDomain_sum {ι} {β : ι → Type v} [∀ i, AddCommMonoid (β i)] {s : Finset γ} {h : γ → Π₀ i, β i}
    {p : ι → Prop} [DecidablePred p] : (∑ c ∈ s, h c).subtypeDomain p = ∑ c ∈ s, (h c).subtypeDomain p :=
  map_sum (subtypeDomainAddMonoidHom β p) _ s

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