inter_right

Mathlib.Data.Multiset.UnionInter

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

English

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

Русский

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

LaTeX

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

Lean4

theorem inter_right [DecidableEq α] (s) : Nodup t → Nodup (s ∩ t) :=
  nodup_of_le inter_le_right

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

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

Разделы

Аффилиация

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