class ToMultiset (C : Type u_1) (α : outParam (Type u_2)) extends Size : Type (max u_1 u_2)

• size : C → ℕ
• isEmpty : C → Bool
• isEmpty_iff_size_eq_zero : ∀ (c : C), isEmpty c = true ↔ size c = 0
• toMultiset : C → Multiset α
• size_eq_card_toMultiset : ∀ (c : C), size c = Multiset.card (toMultiset c)

theorem ToMultiset.size_eq_card_toMultiset {C : Type u_1} {α : outParam (Type u_2)} [self : ToMultiset C α] (c : C) : size c = Multiset.card (toMultiset c)

theorem ToMultiset.lawfulEmptyCollection_iff (C : Type u_1) (α : outParam (Type u_2)) [ToMultiset C α] [EmptyCollection C] : LawfulEmptyCollection C α ↔ toMultiset ∅ = 0

class LawfulEmptyCollection (C : Type u_1) (α : outParam (Type u_2)) [ToMultiset C α] [EmptyCollection C] : Prop

• toMultiset_empty : toMultiset ∅ = 0

@[simp]

theorem LawfulEmptyCollection.toMultiset_empty {C : Type u_1} {α : outParam (Type u_2)} : ∀ {inst : ToMultiset C α} {inst_1 : EmptyCollection C} [self : LawfulEmptyCollection C α], toMultiset ∅ = 0

class ToMultiset.LawfulInsert (C : Type u_1) (α : outParam (Type u_2)) [ToMultiset C α] [Insert α C] : Prop

• toMultiset_insert : ∀ (a : α) (c : C), toMultiset (insert a c) = a ::ₘ toMultiset c

@[simp]

theorem ToMultiset.LawfulInsert.toMultiset_insert {C : Type u_1} {α : outParam (Type u_2)} : ∀ {inst : ToMultiset C α} {inst_1 : Insert α C} [self : ToMultiset.LawfulInsert C α] (a : α) (c : C), toMultiset (insert a c) = a ::ₘ toMultiset c

instance instToMultisetList {α : Type u_1} : ToMultiset (List α) α

Equations

• instToMultisetList = ToMultiset.mk Multiset.ofList ⋯

instance instToMultisetArray {α : Type u_1} : ToMultiset (Array α) α

Equations

• instToMultisetArray = ToMultiset.mk (fun (c : Array α) => ↑c.toList) ⋯

@[instance 100]

instance instMembership_algorithm {C : Type u_2} {α : Type u_3} [ToMultiset C α] : Membership α C

Equations

• instMembership_algorithm = { mem := fun (c : C) (a : α) => a ∈ toMultiset c }

theorem ToMultiset.mem_iff {C : Type u_2} {α : Type u_3} [ToMultiset C α] {c : C} {v : α} : v ∈ c ↔ v ∈ toMultiset c

theorem mem_toMultiset {C : Type u_2} {α : Type u_3} [ToMultiset C α] {c : C} {v : α} : v ∈ toMultiset c ↔ v ∈ c

@[simp]

theorem toMultiset_of_isEmpty {C : Type u_2} {α : Type u_3} [ToMultiset C α] (c : C) (h : isEmpty c = true) : toMultiset c = 0

@[simp]

theorem toMultiset_list {α : Type u_3} (l : List α) : toMultiset l = ↑l

@[simp]

theorem ToMultiset.not_isEmpty_of_mem {C : Type u_2} {α : Type u_3} [ToMultiset C α] {c : C} {v : α} (hv : v ∈ c) : ¬isEmpty c = true

theorem count_toMultiset_eq_zero {C : Type u_2} {α : Type u_3} [ToMultiset C α] [DecidableEq α] {a : α} {c : C} : Multiset.count a (toMultiset c) = 0 ↔ a ∉ c

theorem count_toMultiset_ne_zero {C : Type u_2} {α : Type u_3} [ToMultiset C α] [DecidableEq α] {a : α} {c : C} : Multiset.count a (toMultiset c) ≠ 0 ↔ a ∈ c

class Mergeable (C : Type u_4) (α : outParam (Type u_5)) [ToMultiset C α] : Type u_4

• merge : C → C → C
• toMultiset_merge : ∀ (s t : C), toMultiset (merge s t) = toMultiset s + toMultiset t

@[simp]

theorem Mergeable.toMultiset_merge {C : Type u_4} {α : outParam (Type u_5)} : ∀ {inst : ToMultiset C α} [self : Mergeable C α] (s t : C), toMultiset (merge s t) = toMultiset s + toMultiset t