nodup_iff_count_le_one — Mathlib

English

A list l is nodup iff every element a appears at most once in l, i.e., count a l ≤ 1 for all a, under DecidableEq.

Русский

Список l является нодуп тогда и только тогда, когда для каждого элемента a встречается не более одного раза, то есть count a l ≤ 1 (при решаемости эквивалентности).

LaTeX

$$$ \text{[DecidableEq } \alpha\text{]} \Rightarrow \operatorname{Nodup}(l) \iff \forall a, \operatorname{count}(a,l) \le 1 $$$

Lean4

theorem nodup_iff_count_le_one [DecidableEq α] {l : List α} : Nodup l ↔ ∀ a, count a l ≤ 1 :=
  nodup_iff_sublist.trans <|
    forall_congr' fun a =>
      have : replicate 2 a <+ l ↔ 1 < count a l := replicate_sublist_iff ..
      (not_congr this).trans not_lt

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