mathlib documentation

data.multiset.erase_dup

Erasing duplicates in a multiset. #

erase_dup #

def multiset.erase_dup {α : Type u_1} [decidable_eq α] (s : multiset α) :

erase_dup s removes duplicates from s, yielding a nodup multiset.

Equations

s.erase_dup = quot.lift_on s (λ (l : list α), ↑(l.erase_dup)) multiset.erase_dup._proof_1

@[simp]

theorem multiset.coe_erase_dup {α : Type u_1} [decidable_eq α] (l : list α) :

↑l.erase_dup = ↑(l.erase_dup)

@[simp]

theorem multiset.erase_dup_zero {α : Type u_1} [decidable_eq α] :

0.erase_dup = 0

@[simp]

theorem multiset.mem_erase_dup {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :

a ∈ s.erase_dup ↔ a ∈ s

@[simp]

theorem multiset.erase_dup_cons_of_mem {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :

a ∈ s → (a ::ₘ s).erase_dup = s.erase_dup

@[simp]

theorem multiset.erase_dup_cons_of_not_mem {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :

a ∉ s → (a ::ₘ s).erase_dup = a ::ₘ s.erase_dup

theorem multiset.erase_dup_le {α : Type u_1} [decidable_eq α] (s : multiset α) :

s.erase_dup ≤ s

theorem multiset.erase_dup_subset {α : Type u_1} [decidable_eq α] (s : multiset α) :

s.erase_dup ⊆ s

theorem multiset.subset_erase_dup {α : Type u_1} [decidable_eq α] (s : multiset α) :

s ⊆ s.erase_dup

@[simp]

theorem multiset.erase_dup_subset' {α : Type u_1} [decidable_eq α] {s t : multiset α} :

s.erase_dup ⊆ t ↔ s ⊆ t

@[simp]

theorem multiset.subset_erase_dup' {α : Type u_1} [decidable_eq α] {s t : multiset α} :

s ⊆ t.erase_dup ↔ s ⊆ t

@[simp]

theorem multiset.nodup_erase_dup {α : Type u_1} [decidable_eq α] (s : multiset α) :

s.erase_dup.nodup

theorem multiset.erase_dup_eq_self {α : Type u_1} [decidable_eq α] {s : multiset α} :

s.erase_dup = s ↔ s.nodup

theorem multiset.nodup.erase_dup {α : Type u_1} [decidable_eq α] {s : multiset α} :

s.nodup → s.erase_dup = s

Alias of erase_dup_eq_self.

theorem multiset.erase_dup_eq_zero {α : Type u_1} [decidable_eq α] {s : multiset α} :

s.erase_dup = 0 ↔ s = 0

@[simp]

theorem multiset.erase_dup_singleton {α : Type u_1} [decidable_eq α] {a : α} :

{a}.erase_dup = {a}

theorem multiset.le_erase_dup {α : Type u_1} [decidable_eq α] {s t : multiset α} :

s ≤ t.erase_dup ↔ s ≤ t ∧ s.nodup

theorem multiset.erase_dup_ext {α : Type u_1} [decidable_eq α] {s t : multiset α} :

s.erase_dup = t.erase_dup ↔ ∀ (a : α), a ∈ s ↔ a ∈ t

theorem multiset.erase_dup_map_erase_dup_eq {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (f : α → β) (s : multiset α) :

(multiset.map f s.erase_dup).erase_dup = (multiset.map f s).erase_dup

@[simp]

theorem multiset.erase_dup_nsmul {α : Type u_1} [decidable_eq α] {s : multiset α} {n : ℕ} (h0 : n ≠ 0) :

(n • s).erase_dup = s.erase_dup

theorem multiset.nodup.le_erase_dup_iff_le {α : Type u_1} [decidable_eq α] {s t : multiset α} (hno : s.nodup) :

s ≤ t.erase_dup ↔ s ≤ t

theorem multiset.nodup.le_nsmul_iff_le {α : Type u_1} {s t : multiset α} {n : ℕ} (h : s.nodup) (hn : n ≠ 0) :

s ≤ n • t ↔ s ≤ t