nodup_attach — Mathlib

English

A multiset s has no duplicates if and only if its attached version attach s also has no duplicates. In particular, Nodup(attach s) is equivalent to Nodup(s).

Русский

У множества без повторов при присоединении attach s повторения сохраняются эквивалентно: Nodup(attach s) эквивалентно Nodup(s).

LaTeX

$$$\\operatorname{Nodup}(\\mathrm{attach}(s)) \\iff \\operatorname{Nodup}(s).$$$

Lean4

@[simp]
theorem nodup_attach {s : Multiset α} : Nodup (attach s) ↔ Nodup s :=
  Quot.induction_on s fun _ => List.nodup_attach

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