disjoint_of_nodup_add

Mathlib.Data.Multiset.UnionInter

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

English

If Nodup(s+t) holds, then s and t are disjoint.

Русский

Если в сумме s+t нет повторов, то s и t несовместны.

LaTeX

$$Nodup(s+t) \\Rightarrow Disjoint(s,t)$$

Lean4

theorem disjoint_of_nodup_add {s t : Multiset α} (d : Nodup (s + t)) : Disjoint s t :=
  (nodup_add.1 d).2.2

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

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

Разделы

Аффилиация

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