nodup_cons

Mathlib.Data.Multiset.ZeroCons

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

English

For any a and s, (a ::ₘ s).Nodup holds iff a ∉ s and s.Nodup.

Русский

Для любых a и s, Nodup (a ::ₘ s) тогда и только тогда, когда a не принадлежит s и s без повторений.

LaTeX

$$$(a ::ₘ s).Nodup \iff (a \notin s) \land s.Nodup$$$

Lean4

@[simp]
theorem nodup_cons {a : α} {s : Multiset α} : Nodup (a ::ₘ s) ↔ a ∉ s ∧ Nodup s :=
  Quot.induction_on s fun _ => List.nodup_cons

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

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

Разделы

Аффилиация

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