dedup_subset'

Mathlib.Data.Multiset.Dedup

URI: https://scilib.ai/kg/mathlib#Multiset.dedup_subset'

English

dedup s ⊆ t iff s ⊆ t.

Русский

dedup s ⊆ t эквивалентно s ⊆ t.

LaTeX

$$$\mathrm{dedup}(s) \subseteq t \iff s \subseteq t$$$

Lean4

@[simp]
theorem dedup_subset' {s t : Multiset α} : dedup s ⊆ t ↔ s ⊆ t :=
  ⟨Subset.trans (subset_dedup _), Subset.trans (dedup_subset _)⟩

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

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

Разделы

Аффилиация

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