card_finsuppSum — Mathlib

English

For a finsupp f and a family g, the cardinality of the sum f.sum g equals the sum of the cardinalities of g on each component: card (f.sum g) = f.sum (λ i m, card (g i m)).

Русский

Кардинал суммы соответствует сумме кардиналов по компонентам.

LaTeX

$$$\operatorname{card} (f.sum g) = f.sum (\lambda i m, \operatorname{card} (g i m)).$$$

Lean4

@[simp]
theorem card_finsuppSum [Zero M] (f : ι →₀ M) (g : ι → M → Multiset α) :
    card (f.sum g) = f.sum fun i m ↦ card (g i m) :=
  map_finsuppSum cardHom ..

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