erase

Mathlib.Data.Multiset.AddSub

URI: https://scilib.ai/kg/mathlib#Multiset.Nodup.erase

English

If l is Nodup, then l.erase a is also Nodup.

Русский

Если l является Nodup, то l.erase a тоже Nodup.

LaTeX

$$$$ \text{If } l \text{ is Nodup, then } l-?a \text{ is Nodup} $$$$

Lean4

theorem erase [DecidableEq α] (a : α) {l} : Nodup l → Nodup (l.erase a) :=
  nodup_of_le (erase_le _ _)

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

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

Разделы

Аффилиация

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