le_iff_subset

Mathlib.Data.Multiset.Defs

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

English

For Nodup s, s ≤ t iff s ⊆ t.

Русский

Для Nodup s, s ≤ t эквивалентно s ⊆ t.

LaTeX

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

Lean4

theorem le_iff_subset {s t : Multiset α} : Nodup s → (s ≤ t ↔ s ⊆ t) :=
  Quotient.inductionOn₂ s t fun _ _ d => ⟨subset_of_le, d.subperm⟩

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

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

Разделы

Аффилиация

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