card_erase_of_mem — Mathlib

English

If a ∈ s, then card(s.erase a) = pred(card s).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem card_erase_of_mem {a : α} {s : Multiset α} : a ∈ s → card (s.erase a) = pred (card s) :=
  Quot.inductionOn s fun _l => length_erase_of_mem

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