dedup_eq_self

Mathlib.Data.Multiset.Dedup

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

← MathLib Explorer

English

For every multiset s, dedup(s) = s if and only if s is Nodup.

Русский

Для любого мультимножества s верно: dedup(s) = s тогда и только тогда, когда s без повторов.

LaTeX

$$$$dedup(s) = s \iff Nodup(s)$$$$

Lean4

theorem dedup_eq_self {s : Multiset α} : dedup s = s ↔ Nodup s :=
  ⟨fun e => e ▸ nodup_dedup s, Quot.induction_on s fun _ h => congr_arg ofList h.dedup⟩

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

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

Разделы

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

Аффилиация

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