nodup_iff_le — Mathlib

English

A multiset s has no duplicates if and only if, for every a, the multiset replicate 2 a is not contained in s.

Русский

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

LaTeX

$$$$ \\operatorname{Nodup}(s) \\iff \\forall a, \\neg \\big( \\operatorname{replicate}(2,a) \\le s \\big). $$$$

Lean4

theorem nodup_iff_le {s : Multiset α} : Nodup s ↔ ∀ a : α, ¬a ::ₘ a ::ₘ 0 ≤ s :=
  Quot.induction_on s fun _ =>
    nodup_iff_sublist.trans <| forall_congr' fun a => not_congr (@replicate_le_coe _ a 2 _).symm

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