card_disjSum

Mathlib.Data.Multiset.Sum

URI: https://scilib.ai/kg/mathlib#Multiset.card_disjSum

English

The cardinality of the disjoint sum equals the sum of cardinalities.

Русский

Кардинал сумма дизъюнкции равен сумме кардиналов.

LaTeX

$$$$ \\operatorname{card}(s.\\operatorname{disjSum} t) = \\operatorname{card}(s) + \\operatorname{card}(t) $$$$

Lean4

@[simp]
theorem card_disjSum : Multiset.card (s.disjSum t) = Multiset.card s + Multiset.card t := by
  rw [disjSum, card_add, card_map, card_map]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru