add_iff

Mathlib.Data.Multiset.UnionInter

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

English

Given Nodup s and Nodup t, Nodup(s+t) holds if and only if Disjoint s t.

Русский

При наличии Nodup s и Nodup t, Nodup(s+t) эквивалентно Disjoint s t.

LaTeX

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

Lean4

theorem add_iff (d₁ : Nodup s) (d₂ : Nodup t) : Nodup (s + t) ↔ Disjoint s t := by simp [nodup_add, d₁, d₂]

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

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

Разделы

Аффилиация

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