card_cons

Mathlib.Data.Multiset.ZeroCons

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

English

The cardinality of a consed multiset equals the cardinality of the tail plus one.

Русский

Кардинал множества после добавления элемента равен кардиналу хвоста плюс единица.

LaTeX

$$card(insert(a, s)) = card(s) + 1$$

Lean4

@[simp]
theorem card_cons (a : α) (s : Multiset α) : card (a ::ₘ s) = card s + 1 :=
  Quot.inductionOn s fun _l => rfl

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

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

Разделы

Аффилиация

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