card_erase_add_one — Mathlib

English

If a ∈ s then card(s.erase a) + 1 = card s.

Русский

Если a принадлежит s, то число элементов после стирания a плюс единица равно числу элементов s.

LaTeX

$$$a \in s \Rightarrow \operatorname{card}(s\erase a) + 1 = \operatorname{card}(s)$$$

Lean4

theorem card_erase_add_one {a : α} {s : Multiset α} : a ∈ s → card (s.erase a) + 1 = card s :=
  Quot.inductionOn s fun _l => length_erase_add_one

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