nodup_add

Mathlib.Data.Multiset.UnionInter

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

← MathLib Explorer

English

Nodup(s+t) is equivalent to Nodup(s) ∧ Nodup(t) ∧ Disjoint s t.

Русский

Nodup(s+t) эквивалентно Nodup(s) ∧ Nodup(t) ∧ Disjoint s t.

LaTeX

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

Lean4

theorem nodup_add {s t : Multiset α} : Nodup (s + t) ↔ Nodup s ∧ Nodup t ∧ Disjoint s t :=
  Quotient.inductionOn₂ s t fun _ _ => by simp [nodup_append, disjoint_iff_ne]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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