nodup_iff_count_eq_one — Mathlib

English

A list l is nodup if and only if every element a in l occurs exactly once in l.

Русский

Список l нодуп тогда и только тогда, когда каждый элемент a из l встречается в l ровно один раз.

LaTeX

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

Lean4

theorem nodup_iff_count_eq_one [DecidableEq α] : Nodup l ↔ ∀ a ∈ l, count a l = 1 :=
  nodup_iff_count_le_one.trans <|
    forall_congr' fun _ =>
      ⟨fun H h => H.antisymm (count_pos_iff.mpr h), fun H =>
        if h : _ then (H h).le else (count_eq_zero.mpr h).trans_le (Nat.zero_le 1)⟩

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