le_dedup_self

Mathlib.Data.Multiset.Dedup

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

English

For any s, s ≤ dedup(s) if and only if s is Nodup.

Русский

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

LaTeX

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

Lean4

theorem le_dedup_self {s : Multiset α} : s ≤ dedup s ↔ Nodup s := by rw [le_dedup, and_iff_right le_rfl]

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

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

Разделы

Аффилиация

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