nodup_iff_count_le_one — Mathlib

English

A nodup multiset s is equivalent to every element appearing at most once in s.

Русский

Безповторное мультимножество s эквивалентно тому, что каждый элемент встречается в s не более чем один раз.

LaTeX

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

Lean4

theorem nodup_iff_count_le_one [DecidableEq α] {s : Multiset α} : Nodup s ↔ ∀ a, count a s ≤ 1 :=
  Quot.induction_on s fun _l => by
    simp only [quot_mk_to_coe'', coe_nodup, coe_count]
    exact List.nodup_iff_count_le_one

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