card_sigma — Mathlib

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, (· ∘ ·)]

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