card_join — Mathlib

English

The cardinality of the join of a multiset of multisets S equals the sum of the cardinalities of the elements of S.

Русский

Кардинал объединения join S равен сумме кардиналов элементов S.

LaTeX

$$$\\operatorname{card}(\\operatorname{join}(S)) = \\operatorname{sum}(\\operatorname{map}(\\operatorname{card}, S))$$$

Lean4

@[simp]
theorem card_join (S) : card (@join α S) = sum (map card S) :=
  Multiset.induction_on S (by simp) (by simp)

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