erase_le — Mathlib

English

Let s be a multiset and a an element. Then the multiset obtained by erasing a from s is a submultiset of s.

Русский

Пусть S — мультисет над некоторым множеством. Тогда мультисет, получаемый удалением одного вхождения элемента a из S, является подмножество S.

LaTeX

$$$s\erase a \le s$$$

Lean4

theorem erase_le (a : α) (s : Multiset α) : s.erase a ≤ s :=
  Quot.inductionOn s fun _ => erase_sublist.subperm

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