card_attach

Mathlib.Data.Multiset.Defs

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

English

The cardinality of the attached multiset equals the cardinality of the original multiset: card(attach m) = card m.

Русский

Кардинал прикрепленного мультисета равен кардиналу исходного: card(attach m) = card m.

LaTeX

$$$\\operatorname{card}(\\operatorname{attach}m)=\\operatorname{card}m.$$$

Lean4

@[simp]
theorem card_attach {m : Multiset α} : card (attach m) = card m :=
  card_pmap _ _ _

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

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

Разделы

Аффилиация

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