card_toMultiset — Mathlib

English

For any f : α →₀ ℕ, the cardinality of the multiset represented by f equals the sum of its values, i.e. card(toMultiset f) = ∑ a, f a.

Русский

Пусть f : α →₀ ℕ. Кардинальность мультимножества, соответствующего f, равна сумме значений f, то есть card(toMultiset f) = ∑ a, f(a).

LaTeX

$$$\operatorname{card}\left(\operatorname{toMultiset}(f)\right) = \sum_{a} f(a)$$$

Lean4

@[simp]
theorem card_toMultiset (f : α →₀ ℕ) : Multiset.card (toMultiset f) = f.sum fun _ => id := by
  simp [toMultiset_apply, Function.id_def]

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