val_le_iff_val_subset

Mathlib.Data.Finset.Dedup

URI: https://scilib.ai/kg/mathlib#Finset.val_le_iff_val_subset

English

For a Finset a and Multiset b, a.val ≤ b if and only if a.val ⊆ b.

Русский

Для Finset a и мультимножества b верно: a.val ≤ b тогда, когда a.val ⊆ b.

LaTeX

$$$\\forall {a : \\mathsf{Finset}\\,\\alpha} {b : \\mathsf{Multiset}\\,\\alpha},\\; a.val \\le b \iff a.val \\subseteq b$$$

Lean4

theorem val_le_iff_val_subset {a : Finset α} {b : Multiset α} : a.val ≤ b ↔ a.val ⊆ b :=
  Multiset.le_iff_subset a.nodup

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

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

Разделы

Аффилиация

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