le_dedup_iff_le

Mathlib.Data.Multiset.Dedup

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

English

If s is Nodup, then s ≤ t.dedup iff s ≤ t.

Русский

Если s без повторов, то s ≤ t.dedup эквивалентно s ≤ t.

LaTeX

$$$$s \text{ Nodup} \Rightarrow s \le dedup(t) \iff s \le t$$$$

Lean4

theorem le_dedup_iff_le {s t : Multiset α} (hno : s.Nodup) : s ≤ t.dedup ↔ s ≤ t := by simp [le_dedup, hno]

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

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

Разделы

Аффилиация

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