nodup_powerset — Mathlib

English

The powerset of a multiset has no duplicates if and only if the original multiset has no duplicates.

Русский

У множества подмножеств нет повторов тогда и только тогда, когда само множество без повторов.

LaTeX

$$$\text{Nodup}(\mathrm{powerset}\ s) \iff \text{Nodup}(s)$$$

Lean4

@[simp]
theorem nodup_powerset {s : Multiset α} : Nodup (powerset s) ↔ Nodup s :=
  ⟨fun h => (nodup_of_le (map_single_le_powerset _) h).of_map _,
    Quotient.inductionOn s fun l h =>
      by
      simp only [quot_mk_to_coe, powerset_coe', coe_nodup]
      refine (nodup_sublists'.2 h).map_on ?_
      exact fun x sx y sy e =>
        (h.perm_iff_eq_of_sublist (mem_sublists'.1 sx) (mem_sublists'.1 sy)).1 (Quotient.exact e)⟩

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