card_sub

Mathlib.Data.Multiset.AddSub

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

← MathLib Explorer

English

If t ≤ s, then card(s − t) = card(s) − card(t).

Русский

Если t ⊆ s, тогда |s − t| = |s| − |t|.

LaTeX

$$$$ t \le s \Rightarrow \operatorname{card}(s - t) = \operatorname{card}(s) - \operatorname{card}(t) $$$$

Lean4

@[simp]
theorem card_sub {s t : Multiset α} (h : t ≤ s) : card (s - t) = card s - card t :=
  Nat.eq_sub_of_add_eq <| by rw [← card_add, Multiset.sub_add_cancel h]

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

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

Разделы

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

Аффилиация

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