inter_left

Mathlib.Data.Multiset.UnionInter

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

English

For DecidableEq α, t is fixed and Nodup s implies Nodup (s ∩ t).

Русский

Для фиксированного t с разрешенным равенством, если s не содержит повторов, то s ∩ t тоже не содержит повторов.

LaTeX

$$Nodup s \\Rightarrow Nodup (s ∩ t)$$

Lean4

theorem inter_left [DecidableEq α] (t) : Nodup s → Nodup (s ∩ t) :=
  nodup_of_le inter_le_left

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

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

Разделы

Аффилиация

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