ndinter_le_right

Mathlib.Data.Multiset.FinsetOps

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

English

If s is nodup, then ndinter s t ≤ t.

Русский

Если s без повторов, то ndinter s t ≤ t.

LaTeX

$$$\\mathrm{Nodup}(s) \\Rightarrow \\mathrm{ndinter}(s,t) \\le t$$$

Lean4

theorem ndinter_le_right {s} (t : Multiset α) (d : Nodup s) : ndinter s t ≤ t :=
  (le_iff_subset <| d.ndinter _).2 <| ndinter_subset_right _ _

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

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

Разделы

Аффилиация

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