nodup_iff_ne_cons_cons — Mathlib

English

A multiset s is nodup if and only if for every a and t, s is not equal to a repeated twice followed by t.

Русский

Мультисет s является без повторов тогда и только тогда, когда для каждого a и t множество s не равно a, повторяющемуся дважды, затем t.

LaTeX

$$$$ \\operatorname{Nodup}(s) \\iff \\forall a,t,\\ s \\neq a \\;::ₘ\\; a \\;::ₘ\\; t. $$$$

Lean4

theorem nodup_iff_ne_cons_cons {s : Multiset α} : s.Nodup ↔ ∀ a t, s ≠ a ::ₘ a ::ₘ t :=
  nodup_iff_le.trans
    ⟨fun h a _ s_eq => h a (s_eq.symm ▸ cons_le_cons a (cons_le_cons a (zero_le _))), fun h a le =>
      let ⟨t, s_eq⟩ := le_iff_exists_add.mp le
      h a t (by rwa [cons_add, cons_add, Multiset.zero_add] at s_eq)⟩

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