Erasing duplicates in a multiset. #

dedup #

source

ink

def Multiset.dedup {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) :

Multiset α

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

Equations

Multiset.dedup s = Quot.liftOn s (fun l => ↑(List.dedup l)) (_ : ∀ (x x_1 : List α), Setoid.r x x_1 → Quot.mk Setoid.r (List.dedup x) = Quot.mk Setoid.r (List.dedup x_1))

source

ink

@[simp]

theorem Multiset.coe_dedup {α : Type u_1} [inst : DecidableEq α] (l : List α) :

Multiset.dedup ↑l = ↑(List.dedup l)

source

ink

@[simp]

theorem Multiset.dedup_zero {α : Type u_1} [inst : DecidableEq α] :

Multiset.dedup 0 = 0

source

ink

@[simp]

theorem Multiset.mem_dedup {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α} :

a ∈ Multiset.dedup s ↔ a ∈ s

source

ink

@[simp]

theorem Multiset.dedup_cons_of_mem {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α} :

a ∈ s → Multiset.dedup (a ::ₘ s) = Multiset.dedup s

source

ink

@[simp]

theorem Multiset.dedup_cons_of_not_mem {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α} :

¬a ∈ s → Multiset.dedup (a ::ₘ s) = a ::ₘ Multiset.dedup s

source

ink

theorem Multiset.dedup_le {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) :

Multiset.dedup s ≤ s

source

ink

theorem Multiset.dedup_subset {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) :

Multiset.dedup s ⊆ s

source

ink

theorem Multiset.subset_dedup {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) :

s ⊆ Multiset.dedup s

source

ink

@[simp]

theorem Multiset.dedup_subset' {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {t : Multiset α} :

Multiset.dedup s ⊆ t ↔ s ⊆ t

source

ink

@[simp]

theorem Multiset.subset_dedup' {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {t : Multiset α} :

s ⊆ Multiset.dedup t ↔ s ⊆ t

source

ink

@[simp]

theorem Multiset.nodup_dedup {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) :

Multiset.Nodup (Multiset.dedup s)

source

ink

theorem Multiset.dedup_eq_self {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} :

Multiset.dedup s = s ↔ Multiset.Nodup s

source

ink

theorem Multiset.Nodup.dedup {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} :

Multiset.Nodup s → Multiset.dedup s = s

Alias of the reverse direction of Multiset.dedup_eq_self.

source

ink

theorem Multiset.count_dedup {α : Type u_1} [inst : DecidableEq α] (m : Multiset α) (a : α) :

Multiset.count a (Multiset.dedup m) = if a ∈ m then 1 else 0

source

ink

@[simp]

theorem Multiset.dedup_idempotent {α : Type u_1} [inst : DecidableEq α] {m : Multiset α} :

Multiset.dedup (Multiset.dedup m) = Multiset.dedup m

source

ink

@[simp]

theorem Multiset.dedup_bind_dedup {α : Type u_2} {β : Type u_1} [inst : DecidableEq α] [inst : DecidableEq β] (m : Multiset α) (f : α → Multiset β) :

Multiset.dedup (Multiset.bind (Multiset.dedup m) f) = Multiset.dedup (Multiset.bind m f)

source

ink

theorem Multiset.dedup_eq_zero {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} :

Multiset.dedup s = 0 ↔ s = 0

source

ink

@[simp]

theorem Multiset.dedup_singleton {α : Type u_1} [inst : DecidableEq α] {a : α} :

Multiset.dedup {a} = {a}

source

ink

theorem Multiset.le_dedup {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {t : Multiset α} :

s ≤ Multiset.dedup t ↔ s ≤ t ∧ Multiset.Nodup s

source

ink

theorem Multiset.le_dedup_self {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} :

s ≤ Multiset.dedup s ↔ Multiset.Nodup s

source

ink

theorem Multiset.dedup_ext {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {t : Multiset α} :

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

source

ink

theorem Multiset.dedup_map_dedup_eq {α : Type u_2} {β : Type u_1} [inst : DecidableEq α] [inst : DecidableEq β] (f : α → β) (s : Multiset α) :

Multiset.dedup (Multiset.map f (Multiset.dedup s)) = Multiset.dedup (Multiset.map f s)

source

ink

@[simp]

theorem Multiset.dedup_nsmul {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {n : ℕ} (h0 : n ≠ 0) :

Multiset.dedup (n • s) = Multiset.dedup s

source

ink

theorem Multiset.Nodup.le_dedup_iff_le {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {t : Multiset α} (hno : Multiset.Nodup s) :

s ≤ Multiset.dedup t ↔ s ≤ t

source

ink

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

s ≤ n • t ↔ s ≤ t