class Membership.IsEmpty (C : Type u_3) {α : outParam (Type u_4)} [Membership α C] : Type u_3

• isEmpty : C → Bool
• isEmpty_iff_forall_not_mem {c : C} : isEmpty c = true ↔ ∀ (a : α), ¬a ∈ c

theorem isEmpty_eq_false_iff_exists_mem {C : Type u_1} {α : Type u_2} [Membership α C] [Membership.IsEmpty C] {c : C} : isEmpty c = false ↔ ∃ (a : α), a ∈ c

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, Membership.IsEmpty C : Type (max u_3 u_4)

• mem : C → α → Prop
• isEmpty : C → Bool
• isEmpty_iff_forall_not_mem {c : C} : isEmpty c = true ↔ ∀ (a : α), ¬a ∈ c
• toMultiset : C → Multiset α
• mem_toMultiset {x : α} {c : C} : x ∈ toMultiset c ↔ x ∈ c

def sizeTM {C : Type u_1} {α : Type u_2} [ToMultiset C α] (c : C) : ℕ

The size function derived from ToMultiset.

Use size for computation whenever possible, as it is usually faster.

Equations

• sizeTM c = (toMultiset c).card

theorem card_toMultiset {C : Type u_1} {α : Type u_2} [ToMultiset C α] (c : C) : (toMultiset c).card = sizeTM c

theorem sizeTM_eq_card_toMultiset {C : Type u_1} {α : Type u_2} [ToMultiset C α] (c : C) : sizeTM c = (toMultiset c).card

class Size (C : Type u_3) {α : outParam (Type u_4)} [ToMultiset C α] : Type u_3

• size : C → ℕ
• size_eq_sizeTM (c : C) : size c = sizeTM 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 [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 instIsEmptyList {α : Type u_2} : Membership.IsEmpty (List α)

Equations

• instIsEmptyList = { isEmpty := List.isEmpty, isEmpty_iff_forall_not_mem := ⋯ }

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

Equations

• instToMultisetList = { toMembership := List.instMembership, toIsEmpty := instIsEmptyList, toMultiset := Multiset.ofList, mem_toMultiset := ⋯ }

instance instSizeList {α : Type u_2} : Size (List α)

Equations

• instSizeList = { size := List.length, size_eq_sizeTM := ⋯ }

instance instIsEmptyArray {α : Type u_2} : Membership.IsEmpty (Array α)

Equations

• instIsEmptyArray = { isEmpty := Array.isEmpty, isEmpty_iff_forall_not_mem := ⋯ }

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

Equations

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

instance instSizeArray {α : Type u_2} : Size (Array α)

Equations

• instSizeArray = { size := Array.size, size_eq_sizeTM := ⋯ }

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_list {α : Type u_2} (l : List α) : toMultiset l = ↑l

theorem isEmpty_iff_sizeTM_eq_zero {C : Type u_1} {α : Type u_2} [ToMultiset C α] {c : C} : isEmpty c = true ↔ sizeTM c = 0

theorem isEmpty_iff_size_eq_zero {C : Type u_1} {α : Type u_2} [ToMultiset C α] [Size C] {c : C} : isEmpty c = true ↔ size c = 0

theorem isEmpty_eq_decide_sizeTM {C : Type u_1} {α : Type u_2} [ToMultiset C α] (c : C) : isEmpty c = decide (sizeTM c = 0)

theorem isEmpty_eq_sizeTM_beq_zero {C : Type u_1} {α : Type u_2} [ToMultiset C α] (c : C) : isEmpty c = (sizeTM c == 0)

theorem toMultiset_iff_isEmpty {C : Type u_1} {α : Type u_2} [ToMultiset C α] {c : C} : isEmpty c = true ↔ toMultiset c = 0

@[simp]

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

Alias of the forward direction of toMultiset_iff_isEmpty.

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