class LawfulEmptyCollection (C : Type u_3) (α : outParam (Type u_4)) [Membership α C] [EmptyCollection C] : Prop

• not_mem_empty : ∀ (x : α), x ∉ ∅

theorem lawfulEmptyCollection_iff (C : Type u_3) (α : outParam (Type u_4)) [Membership α C] [EmptyCollection C] : LawfulEmptyCollection C α ↔ ∀ (x : α), x ∉ ∅

class ToMultiset (C : Type u_3) (α : outParam (Type u_4)) extends Membership α C, Size C : Type (max u_3 u_4)

• mem : C → α → Prop
• size : C → ℕ
• isEmpty : C → Bool
• isEmpty_iff_size_eq_zero : ∀ {c : C}, isEmpty c = true ↔ size c = 0
• toMultiset : C → Multiset α
• mem_toMultiset : ∀ {x : α} {c : C}, x ∈ toMultiset c ↔ x ∈ c
• size_eq_card_toMultiset : ∀ (c : C), size c = Multiset.card (toMultiset c)

class ToMultiset.LawfulInsert (C : Type u_3) (α : outParam (Type u_4)) [ToMultiset C α] [Insert α C] : Prop

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

class LawfulErase (C : Type u_3) (α : outParam (Type u_4)) [ToMultiset C α] [Erase C α] : Prop

• toMultiset_erase : ∀ [inst : DecidableEq α] (c : C) (a : α), toMultiset (erase c a) = (toMultiset c).erase a

theorem lawfulErase_iff_toMultiset (C : Type u_3) (α : outParam (Type u_4)) [ToMultiset C α] [Erase C α] : LawfulErase C α ↔ ∀ [inst : DecidableEq α] (c : C) (a : α), toMultiset (erase c a) = (toMultiset c).erase a

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

Equations

• instToMultisetList = ToMultiset.mk Multiset.ofList ⋯ ⋯

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

Equations

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

theorem lawfulEmptyCollection_iff_toMultiset {C : Type u_1} {α : Type u_2} [ToMultiset C α] [EmptyCollection C] : LawfulEmptyCollection C α ↔ toMultiset ∅ = 0

theorem LawfulEmptyCollection.of_toMultiset {C : Type u_1} {α : Type u_2} [ToMultiset C α] [EmptyCollection C] : toMultiset ∅ = 0 → LawfulEmptyCollection C α

Alias of the reverse direction of lawfulEmptyCollection_iff_toMultiset.

@[simp]

theorem toMultiset_empty {C : Type u_1} {α : Type u_2} [ToMultiset C α] [EmptyCollection C] [LawfulEmptyCollection C α] : toMultiset ∅ = 0

@[simp]

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

@[simp]

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

@[simp]

theorem ToMultiset.not_isEmpty_of_mem {C : Type u_1} {α : Type u_2} [ToMultiset C α] {c : C} {x : α} (hx : x ∈ c) : ¬isEmpty c = true

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

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

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

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