card_erase_eq_ite

Mathlib.Data.Multiset.AddSub

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

← MathLib Explorer

English

card(s.erase a) = ite(a ∈ s, pred(card s), card s).

Русский

card(s.erase a) равно ite(a ∈ s, pred(card s), card s).

LaTeX

$$$card(s.erase a) = \operatorname{ite}(a \in s, \operatorname{pred}(card\s), card(s))$$$

Lean4

theorem card_erase_eq_ite {a : α} {s : Multiset α} : card (s.erase a) = if a ∈ s then pred (card s) else card s :=
  by
  by_cases h : a ∈ s
  · rwa [card_erase_of_mem h, if_pos]
  · rwa [erase_of_notMem h, if_neg]

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

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

Разделы

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

Аффилиация

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