nodup_iff_count_eq_one — Mathlib

English

A nodup multiset s satisfies that every a ∈ s has count(a, s) = 1.

Русский

Мультимножество без повторов имеет кратность каждого элемента равной 1.

LaTeX

$$$\operatorname{Nodup}(s) \iff \forall a \in s, \operatorname{count}(a, s) = 1$$$

Lean4

theorem nodup_iff_count_eq_one [DecidableEq α] : Nodup s ↔ ∀ a ∈ s, count a s = 1 :=
  Quot.induction_on s fun _l => by simpa using List.nodup_iff_count_eq_one

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