nodup_iff_pairwise — Mathlib

English

A multiset s has no duplicates if and only if all its elements are pairwise distinct.

Русский

Мультсет s не содержит повторяющихся элементов тогда и только тогда, когда его элементы попарно различны.

LaTeX

$$$$ \\operatorname{Nodup}(s) \\iff \\operatorname{Pairwise}(\\neq)\\, s. $$$$

Lean4

theorem nodup_iff_pairwise {α} {s : Multiset α} : Nodup s ↔ Pairwise (· ≠ ·) s :=
  Quotient.inductionOn s fun _ => (pairwise_coe_iff_pairwise fun _ _ => Ne.symm).symm

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