count_erase_self

Mathlib.Data.Multiset.AddSub

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

← MathLib Explorer

English

count a (erase s a) = count a s - 1.

Русский

count a (erase s a) = count a s - 1.

LaTeX

$$$\operatorname{count}(a, \operatorname{erase}(s, a)) = \operatorname{count}(a, s) - 1$$$

Lean4

@[simp]
theorem count_erase_self (a : α) (s : Multiset α) : count a (erase s a) = count a s - 1 :=
  Quotient.inductionOn s fun l => by convert List.count_erase_self (a := a) (l := l) <;> rw [← coe_count] <;> simp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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