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 = (toMultiset c).card

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 [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 = { toMembership := List.instMembership, toSize := instSizeList, toMultiset := Multiset.ofList, mem_toMultiset := ⋯, size_eq_card_toMultiset := ⋯ }

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

Equations

• instToMultisetArray = { toMembership := Array.instMembership, toSize := instSizeArray, toMultiset := fun (c : Array α) => ↑c.toList, mem_toMultiset := ⋯, size_eq_card_toMultiset := ⋯ }

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