English
The cardinality of s.sigma t equals the sum over s of the cardinalities of t a: card (s.sigma t) = sum (map (λ a, card (t a)) s).
Русский
Кардинальность s.sigma t равна сумме по s кардинальностей t a: card (s.sigma t) = sum (map (λ a, card (t a)) s).
LaTeX
$$$\mathrm{card}(s.\sigma t) = \sum (\mathrm{map}(\lambda a. \mathrm{card}(t a))\ s)$$$
Lean4
@[simp]
theorem card_sigma : card (s.sigma t) = sum (map (fun a => card (t a)) s) := by simp [Multiset.sigma, (· ∘ ·)]