Multisets

Multisets are finite sets with duplicates allowed. They are implemented here as the quotient of lists by permutation. This gives them computational content.

Notation

• 0: The empty multiset.
• {a}: The multiset containing a single occurrence of a.
• a ::ₘ s: The multiset containing one more occurrence of a than s does.
• s + t: The multiset for which the number of occurrences of each a is the sum of the occurrences of a in s and t.
• s - t: The multiset for which the number of occurrences of each a is the difference of the occurrences of a in s and t.
• s ∪ t: The multiset for which the number of occurrences of each a is the max of the occurrences of a in s and t.
• s ∩ t: The multiset for which the number of occurrences of each a is the min of the occurrences of a in s and t.

def Multiset (α : Type u) : Type u

Multiset α is the quotient of List α by list permutation. The result is a type of finite sets with duplicates allowed.

Equations

• Multiset α = Quotient (List.isSetoid α)

def Multiset.ofList {α : Type u_1} : List α → Multiset α

The quotient map from List α to Multiset α.

Equations

• Multiset.ofList = Quot.mk ⇑(List.isSetoid α)

instance Multiset.instCoeList {α : Type u_1} : Coe (List α) (Multiset α)

Equations

• Multiset.instCoeList = { coe := Multiset.ofList }

@[simp]

theorem Multiset.quot_mk_to_coe {α : Type u_1} (l : List α) : ⟦l⟧ = ↑l

@[simp]

theorem Multiset.quot_mk_to_coe' {α : Type u_1} (l : List α) : Quot.mk (fun (x1 x2 : List α) => x1 ≈ x2) l = ↑l

@[simp]

theorem Multiset.quot_mk_to_coe'' {α : Type u_1} (l : List α) : Quot.mk (⇑(List.isSetoid α)) l = ↑l

@[simp]

theorem Multiset.lift_coe {α : Type u_3} {β : Type u_4} (x : List α) (f : List α → β) (h : ∀ (a b : List α), a ≈ b → f a = f b) : Quotient.lift f h ↑x = f x

@[simp]

theorem Multiset.coe_eq_coe {α : Type u_1} {l₁ l₂ : List α} : ↑l₁ = ↑l₂ ↔ l₁.Perm l₂

instance Multiset.instDecidableEquivListOfDecidableEq {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ ≈ l₂)

Equations

• Multiset.instDecidableEquivListOfDecidableEq l₁ l₂ = inferInstanceAs (Decidable (l₁.Perm l₂))

instance Multiset.instDecidableRListOfDecidableEq {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) : Decidable ((List.isSetoid α) l₁ l₂)

Equations

• Multiset.instDecidableRListOfDecidableEq l₁ l₂ = inferInstanceAs (Decidable (l₁.Perm l₂))

instance Multiset.decidableEq {α : Type u_1} [DecidableEq α] : DecidableEq (Multiset α)

Equations

• x✝¹.decidableEq x✝ = Quotient.recOnSubsingleton₂ x✝¹ x✝ fun (x x_1 : List α) => decidable_of_iff' (x ≈ x_1) ⋯

def Multiset.sizeOf {α : Type u_1} [SizeOf α] (s : Multiset α) : ℕ

defines a size for a multiset by referring to the size of the underlying list

Equations

• s.sizeOf = Quot.liftOn s sizeOf ⋯

instance Multiset.instSizeOf {α : Type u_1} [SizeOf α] : SizeOf (Multiset α)

Equations

• Multiset.instSizeOf = { sizeOf := Multiset.sizeOf }

Empty multiset

def Multiset.zero {α : Type u_1} : Multiset α

0 : Multiset α is the empty set

Equations

• Multiset.zero = ↑[]

instance Multiset.instZero {α : Type u_1} : Zero (Multiset α)

Equations

• Multiset.instZero = { zero := Multiset.zero }

instance Multiset.instEmptyCollection {α : Type u_1} : EmptyCollection (Multiset α)

Equations

• Multiset.instEmptyCollection = { emptyCollection := 0 }

instance Multiset.inhabitedMultiset {α : Type u_1} : Inhabited (Multiset α)

Equations

• Multiset.inhabitedMultiset = { default := 0 }

instance Multiset.instUniqueOfIsEmpty {α : Type u_1} [IsEmpty α] : Unique (Multiset α)

Equations

• Multiset.instUniqueOfIsEmpty = { default := 0, uniq := ⋯ }

@[simp]

theorem Multiset.coe_nil {α : Type u_1} : ↑[] = 0

@[simp]

theorem Multiset.empty_eq_zero {α : Type u_1} : ∅ = 0

@[simp]

theorem Multiset.coe_eq_zero {α : Type u_1} (l : List α) : ↑l = 0 ↔ l = []

theorem Multiset.coe_eq_zero_iff_isEmpty {α : Type u_1} (l : List α) : ↑l = 0 ↔ l.isEmpty = true

Multiset.cons

def Multiset.cons {α : Type u_1} (a : α) (s : Multiset α) : Multiset α

cons a s is the multiset which contains s plus one more instance of a.

Equations

• a ::ₘ s = Quot.liftOn s (fun (l : List α) => ↑(a :: l)) ⋯

def Multiset.«term_::ₘ_» : Lean.TrailingParserDescr

cons a s is the multiset which contains s plus one more instance of a.

Equations

• Multiset.«term_::ₘ_» = Lean.ParserDescr.trailingNode `Multiset.«term_::ₘ_» 67 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ::ₘ ") (Lean.ParserDescr.cat `term 67))

instance Multiset.instInsert {α : Type u_1} : Insert α (Multiset α)

Equations

• Multiset.instInsert = { insert := Multiset.cons }

@[simp]

theorem Multiset.insert_eq_cons {α : Type u_1} (a : α) (s : Multiset α) : insert a s = a ::ₘ s

@[simp]

theorem Multiset.cons_coe {α : Type u_1} (a : α) (l : List α) : a ::ₘ ↑l = ↑(a :: l)

@[simp]

theorem Multiset.cons_inj_left {α : Type u_1} {a b : α} (s : Multiset α) : a ::ₘ s = b ::ₘ s ↔ a = b

@[simp]

theorem Multiset.cons_inj_right {α : Type u_1} (a : α) {s t : Multiset α} : a ::ₘ s = a ::ₘ t ↔ s = t

theorem Multiset.induction {α : Type u_1} {p : Multiset α → Prop} (empty : p 0) (cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)) (s : Multiset α) : p s

theorem Multiset.induction_on {α : Type u_1} {p : Multiset α → Prop} (s : Multiset α) (empty : p 0) (cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)) : p s

theorem Multiset.cons_swap {α : Type u_1} (a b : α) (s : Multiset α) : a ::ₘ b ::ₘ s = b ::ₘ a ::ₘ s

def Multiset.rec {α : Type u_1} {C : Multiset α → Sort u_3} (C_0 : C 0) (C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)) (C_cons_heq : ∀ (a a' : α) (m : Multiset α) (b : C m), HEq (C_cons a (a' ::ₘ m) (C_cons a' m b)) (C_cons a' (a ::ₘ m) (C_cons a m b))) (m : Multiset α) : C m

Dependent recursor on multisets. TODO: should be @[recursor 6], but then the definition of Multiset.pi fails with a stack overflow in whnf.

Equations

• Multiset.rec C_0 C_cons C_cons_heq m = Quotient.hrecOn m (List.rec C_0 fun (a : α) (l : List α) (b : C ⟦l⟧) => C_cons a ⟦l⟧ b) ⋯

def Multiset.recOn {α : Type u_1} {C : Multiset α → Sort u_3} (m : Multiset α) (C_0 : C 0) (C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)) (C_cons_heq : ∀ (a a' : α) (m : Multiset α) (b : C m), HEq (C_cons a (a' ::ₘ m) (C_cons a' m b)) (C_cons a' (a ::ₘ m) (C_cons a m b))) : C m

Companion to Multiset.rec with more convenient argument order.

Equations

• m.recOn C_0 C_cons C_cons_heq = Multiset.rec C_0 C_cons C_cons_heq m

@[simp]

theorem Multiset.recOn_0 {α : Type u_1} {C : Multiset α → Sort u_3} {C_0 : C 0} {C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)} {C_cons_heq : ∀ (a a' : α) (m : Multiset α) (b : C m), HEq (C_cons a (a' ::ₘ m) (C_cons a' m b)) (C_cons a' (a ::ₘ m) (C_cons a m b))} : Multiset.recOn 0 C_0 C_cons C_cons_heq = C_0

@[simp]

theorem Multiset.recOn_cons {α : Type u_1} {C : Multiset α → Sort u_3} {C_0 : C 0} {C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)} {C_cons_heq : ∀ (a a' : α) (m : Multiset α) (b : C m), HEq (C_cons a (a' ::ₘ m) (C_cons a' m b)) (C_cons a' (a ::ₘ m) (C_cons a m b))} (a : α) (m : Multiset α) : (a ::ₘ m).recOn C_0 C_cons C_cons_heq = C_cons a m (m.recOn C_0 C_cons C_cons_heq)

def Multiset.Mem {α : Type u_1} (s : Multiset α) (a : α) : Prop

a ∈ s means that a has nonzero multiplicity in s.

Equations

• s.Mem a = Quot.liftOn s (fun (l : List α) => a ∈ l) ⋯

instance Multiset.instMembership {α : Type u_1} : Membership α (Multiset α)

Equations

• Multiset.instMembership = { mem := Multiset.Mem }

@[simp]

theorem Multiset.mem_coe {α : Type u_1} {a : α} {l : List α} : a ∈ ↑l ↔ a ∈ l

instance Multiset.decidableMem {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) : Decidable (a ∈ s)

Equations

• Multiset.decidableMem a s = Quot.recOnSubsingleton s fun (l : List α) => inferInstanceAs (Decidable (a ∈ l))

@[simp]

theorem Multiset.mem_cons {α : Type u_1} {a b : α} {s : Multiset α} : a ∈ b ::ₘ s ↔ a = b ∨ a ∈ s

theorem Multiset.mem_cons_of_mem {α : Type u_1} {a b : α} {s : Multiset α} (h : a ∈ s) : a ∈ b ::ₘ s

theorem Multiset.mem_cons_self {α : Type u_1} (a : α) (s : Multiset α) : a ∈ a ::ₘ s

theorem Multiset.forall_mem_cons {α : Type u_1} {p : α → Prop} {a : α} {s : Multiset α} : (∀ x ∈ a ::ₘ s, p x) ↔ p a ∧ ∀ x ∈ s, p x

theorem Multiset.exists_cons_of_mem {α : Type u_1} {s : Multiset α} {a : α} : a ∈ s → ∃ (t : Multiset α), s = a ::ₘ t

@[simp]

theorem Multiset.not_mem_zero {α : Type u_1} (a : α) : a ∉ 0

theorem Multiset.eq_zero_of_forall_not_mem {α : Type u_1} {s : Multiset α} : (∀ (x : α), x ∉ s) → s = 0

theorem Multiset.eq_zero_iff_forall_not_mem {α : Type u_1} {s : Multiset α} : s = 0 ↔ ∀ (a : α), a ∉ s

theorem Multiset.exists_mem_of_ne_zero {α : Type u_1} {s : Multiset α} : s ≠ 0 → ∃ (a : α), a ∈ s

theorem Multiset.empty_or_exists_mem {α : Type u_1} (s : Multiset α) : s = 0 ∨ ∃ (a : α), a ∈ s

@[simp]

theorem Multiset.zero_ne_cons {α : Type u_1} {a : α} {m : Multiset α} : 0 ≠ a ::ₘ m

@[simp]

theorem Multiset.cons_ne_zero {α : Type u_1} {a : α} {m : Multiset α} : a ::ₘ m ≠ 0

theorem Multiset.cons_eq_cons {α : Type u_1} {a b : α} {as bs : Multiset α} : a ::ₘ as = b ::ₘ bs ↔ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs

Singleton

instance Multiset.instSingleton {α : Type u_1} : Singleton α (Multiset α)

Equations

• Multiset.instSingleton = { singleton := fun (a : α) => a ::ₘ 0 }

instance Multiset.instLawfulSingleton {α : Type u_1} : LawfulSingleton α (Multiset α)

@[simp]

theorem Multiset.cons_zero {α : Type u_1} (a : α) : a ::ₘ 0 = {a}

@[simp]

theorem Multiset.coe_singleton {α : Type u_1} (a : α) : ↑[a] = {a}

@[simp]

theorem Multiset.mem_singleton {α : Type u_1} {a b : α} : b ∈ {a} ↔ b = a

theorem Multiset.mem_singleton_self {α : Type u_1} (a : α) : a ∈ {a}

@[simp]

theorem Multiset.singleton_inj {α : Type u_1} {a b : α} : {a} = {b} ↔ a = b

@[simp]

theorem Multiset.coe_eq_singleton {α : Type u_1} {l : List α} {a : α} : ↑l = {a} ↔ l = [a]

@[simp]

theorem Multiset.singleton_eq_cons_iff {α : Type u_1} {a b : α} (m : Multiset α) : {a} = b ::ₘ m ↔ a = b ∧ m = 0

theorem Multiset.pair_comm {α : Type u_1} (x y : α) : {x, y} = {y, x}

Multiset.Subset

def Multiset.Subset {α : Type u_1} (s t : Multiset α) : Prop

s ⊆ t is the lift of the list subset relation. It means that any element with nonzero multiplicity in s has nonzero multiplicity in t, but it does not imply that the multiplicity of a in s is less or equal than in t; see s ≤ t for this relation.

Equations

• s.Subset t = ∀ ⦃a : α⦄, a ∈ s → a ∈ t

instance Multiset.instHasSubset {α : Type u_1} : HasSubset (Multiset α)

Equations

• Multiset.instHasSubset = { Subset := Multiset.Subset }

instance Multiset.instHasSSubset {α : Type u_1} : HasSSubset (Multiset α)

Equations

• Multiset.instHasSSubset = { SSubset := fun (s t : Multiset α) => s ⊆ t ∧ ¬t ⊆ s }

instance Multiset.instIsNonstrictStrictOrder {α : Type u_1} : IsNonstrictStrictOrder (Multiset α) (fun (x1 x2 : Multiset α) => x1 ⊆ x2) fun (x1 x2 : Multiset α) => x1 ⊂ x2

@[simp]

theorem Multiset.coe_subset {α : Type u_1} {l₁ l₂ : List α} : ↑l₁ ⊆ ↑l₂ ↔ l₁ ⊆ l₂

@[simp]

theorem Multiset.Subset.refl {α : Type u_1} (s : Multiset α) : s ⊆ s

theorem Multiset.Subset.trans {α : Type u_1} {s t u : Multiset α} : s ⊆ t → t ⊆ u → s ⊆ u

theorem Multiset.subset_iff {α : Type u_1} {s t : Multiset α} : s ⊆ t ↔ ∀ ⦃x : α⦄, x ∈ s → x ∈ t

theorem Multiset.mem_of_subset {α : Type u_1} {s t : Multiset α} {a : α} (h : s ⊆ t) : a ∈ s → a ∈ t

@[simp]

theorem Multiset.zero_subset {α : Type u_1} (s : Multiset α) : 0 ⊆ s

theorem Multiset.subset_cons {α : Type u_1} (s : Multiset α) (a : α) : s ⊆ a ::ₘ s

theorem Multiset.ssubset_cons {α : Type u_1} {s : Multiset α} {a : α} (ha : a ∉ s) : s ⊂ a ::ₘ s

@[simp]

theorem Multiset.cons_subset {α : Type u_1} {a : α} {s t : Multiset α} : a ::ₘ s ⊆ t ↔ a ∈ t ∧ s ⊆ t

theorem Multiset.cons_subset_cons {α : Type u_1} {a : α} {s t : Multiset α} : s ⊆ t → a ::ₘ s ⊆ a ::ₘ t

theorem Multiset.eq_zero_of_subset_zero {α : Type u_1} {s : Multiset α} (h : s ⊆ 0) : s = 0

@[simp]

theorem Multiset.subset_zero {α : Type u_1} {s : Multiset α} : s ⊆ 0 ↔ s = 0

@[simp]

theorem Multiset.zero_ssubset {α : Type u_1} {s : Multiset α} : 0 ⊂ s ↔ s ≠ 0

@[simp]

theorem Multiset.singleton_subset {α : Type u_1} {s : Multiset α} {a : α} : {a} ⊆ s ↔ a ∈ s

theorem Multiset.induction_on' {α : Type u_1} {p : Multiset α → Prop} (S : Multiset α) (h₁ : p 0) (h₂ : ∀ {a : α} {s : Multiset α}, a ∈ S → s ⊆ S → p s → p (insert a s)) : p S

Multiset.toList

noncomputable def Multiset.toList {α : Type u_1} (s : Multiset α) : List α

Produces a list of the elements in the multiset using choice.

Equations

• s.toList = Quotient.out s

@[simp]

theorem Multiset.coe_toList {α : Type u_1} (s : Multiset α) : ↑s.toList = s

@[simp]

theorem Multiset.toList_eq_nil {α : Type u_1} {s : Multiset α} : s.toList = [] ↔ s = 0

theorem Multiset.empty_toList {α : Type u_1} {s : Multiset α} : s.toList.isEmpty = true ↔ s = 0

@[simp]

theorem Multiset.toList_zero {α : Type u_1} : toList 0 = []

@[simp]

theorem Multiset.mem_toList {α : Type u_1} {a : α} {s : Multiset α} : a ∈ s.toList ↔ a ∈ s

@[simp]

theorem Multiset.toList_eq_singleton_iff {α : Type u_1} {a : α} {m : Multiset α} : m.toList = [a] ↔ m = {a}

@[simp]

theorem Multiset.toList_singleton {α : Type u_1} (a : α) : {a}.toList = [a]

Partial order on Multisets

def Multiset.Le {α : Type u_1} (s t : Multiset α) : Prop

s ≤ t means that s is a sublist of t (up to permutation). Equivalently, s ≤ t means that count a s ≤ count a t for all a.

Equations

• s.Le t = Quotient.liftOn₂ s t (fun (x1 x2 : List α) => x1.Subperm x2) ⋯

instance Multiset.instPartialOrder {α : Type u_1} : PartialOrder (Multiset α)

Equations

• Multiset.instPartialOrder = PartialOrder.mk ⋯

instance Multiset.decidableLE {α : Type u_1} [DecidableEq α] : DecidableRel fun (x1 x2 : Multiset α) => x1 ≤ x2

Equations

• s.decidableLE t = Quotient.recOnSubsingleton₂ s t List.decidableSubperm

theorem Multiset.subset_of_le {α : Type u_1} {s t : Multiset α} : s ≤ t → s ⊆ t

theorem Multiset.Le.subset {α : Type u_1} {s t : Multiset α} : s ≤ t → s ⊆ t

Alias of Multiset.subset_of_le.

theorem Multiset.mem_of_le {α : Type u_1} {s t : Multiset α} {a : α} (h : s ≤ t) : a ∈ s → a ∈ t

theorem Multiset.not_mem_mono {α : Type u_1} {s t : Multiset α} {a : α} (h : s ⊆ t) : a ∉ t → a ∉ s

@[simp]

theorem Multiset.coe_le {α : Type u_1} {l₁ l₂ : List α} : ↑l₁ ≤ ↑l₂ ↔ l₁.Subperm l₂

theorem Multiset.leInductionOn {α : Type u_1} {C : Multiset α → Multiset α → Prop} {s t : Multiset α} (h : s ≤ t) (H : ∀ {l₁ l₂ : List α}, l₁.Sublist l₂ → C ↑l₁ ↑l₂) : C s t

theorem Multiset.zero_le {α : Type u_1} (s : Multiset α) : 0 ≤ s

instance Multiset.instOrderBot {α : Type u_1} : OrderBot (Multiset α)

Equations

• Multiset.instOrderBot = OrderBot.mk ⋯

@[simp]

theorem Multiset.bot_eq_zero {α : Type u_1} : ⊥ = 0

This is a rfl and simp version of bot_eq_zero.

theorem Multiset.le_zero {α : Type u_1} {s : Multiset α} : s ≤ 0 ↔ s = 0

theorem Multiset.lt_cons_self {α : Type u_1} (s : Multiset α) (a : α) : s < a ::ₘ s

theorem Multiset.le_cons_self {α : Type u_1} (s : Multiset α) (a : α) : s ≤ a ::ₘ s

theorem Multiset.cons_le_cons_iff {α : Type u_1} {s t : Multiset α} (a : α) : a ::ₘ s ≤ a ::ₘ t ↔ s ≤ t

theorem Multiset.cons_le_cons {α : Type u_1} {s t : Multiset α} (a : α) : s ≤ t → a ::ₘ s ≤ a ::ₘ t

@[simp]

theorem Multiset.cons_lt_cons_iff {α : Type u_1} {s t : Multiset α} {a : α} : a ::ₘ s < a ::ₘ t ↔ s < t

theorem Multiset.cons_lt_cons {α : Type u_1} {s t : Multiset α} (a : α) (h : s < t) : a ::ₘ s < a ::ₘ t

theorem Multiset.le_cons_of_not_mem {α : Type u_1} {s t : Multiset α} {a : α} (m : a ∉ s) : s ≤ a ::ₘ t ↔ s ≤ t

theorem Multiset.cons_le_of_not_mem {α : Type u_1} {s t : Multiset α} {a : α} (hs : a ∉ s) : a ::ₘ s ≤ t ↔ a ∈ t ∧ s ≤ t

@[simp]

theorem Multiset.singleton_ne_zero {α : Type u_1} (a : α) : {a} ≠ 0

@[simp]

theorem Multiset.zero_ne_singleton {α : Type u_1} (a : α) : 0 ≠ {a}

@[simp]

theorem Multiset.singleton_le {α : Type u_1} {a : α} {s : Multiset α} : {a} ≤ s ↔ a ∈ s

@[simp]

theorem Multiset.le_singleton {α : Type u_1} {s : Multiset α} {a : α} : s ≤ {a} ↔ s = 0 ∨ s = {a}

@[simp]

theorem Multiset.lt_singleton {α : Type u_1} {s : Multiset α} {a : α} : s < {a} ↔ s = 0

@[simp]

theorem Multiset.ssubset_singleton_iff {α : Type u_1} {s : Multiset α} {a : α} : s ⊂ {a} ↔ s = 0

Additive monoid

def Multiset.add {α : Type u_1} (s₁ s₂ : Multiset α) : Multiset α

The sum of two multisets is the lift of the list append operation. This adds the multiplicities of each element, i.e. count a (s + t) = count a s + count a t.

Equations

• s₁.add s₂ = Quotient.liftOn₂ s₁ s₂ (fun (l₁ l₂ : List α) => ↑(l₁ ++ l₂)) ⋯

instance Multiset.instAdd {α : Type u_1} : Add (Multiset α)

Equations

• Multiset.instAdd = { add := Multiset.add }

@[simp]

theorem Multiset.coe_add {α : Type u_1} (s t : List α) : ↑s + ↑t = ↑(s ++ t)

@[simp]

theorem Multiset.singleton_add {α : Type u_1} (a : α) (s : Multiset α) : {a} + s = a ::ₘ s

theorem Multiset.add_le_add_iff_left {α : Type u_1} {s t u : Multiset α} : s + t ≤ s + u ↔ t ≤ u

theorem Multiset.add_le_add_iff_right {α : Type u_1} {s t u : Multiset α} : s + u ≤ t + u ↔ s ≤ t

theorem Multiset.add_le_add_left {α : Type u_1} {s t u : Multiset α} : t ≤ u → s + t ≤ s + u

Alias of the reverse direction of Multiset.add_le_add_iff_left.

theorem Multiset.le_of_add_le_add_left {α : Type u_1} {s t u : Multiset α} : s + t ≤ s + u → t ≤ u

Alias of the forward direction of Multiset.add_le_add_iff_left.

theorem Multiset.le_of_add_le_add_right {α : Type u_1} {s t u : Multiset α} : s + u ≤ t + u → s ≤ t

Alias of the forward direction of Multiset.add_le_add_iff_right.

theorem Multiset.add_le_add_right {α : Type u_1} {s t u : Multiset α} : s ≤ t → s + u ≤ t + u

Alias of the reverse direction of Multiset.add_le_add_iff_right.

theorem Multiset.add_comm {α : Type u_1} (s t : Multiset α) : s + t = t + s

theorem Multiset.add_assoc {α : Type u_1} (s t u : Multiset α) : s + t + u = s + (t + u)

@[simp]

theorem Multiset.zero_add {α : Type u_1} (s : Multiset α) : 0 + s = s

@[simp]

theorem Multiset.add_zero {α : Type u_1} (s : Multiset α) : s + 0 = s

theorem Multiset.le_add_right {α : Type u_1} (s t : Multiset α) : s ≤ s + t

theorem Multiset.le_add_left {α : Type u_1} (s t : Multiset α) : s ≤ t + s

theorem Multiset.subset_add_left {α : Type u_1} {s t : Multiset α} : s ⊆ s + t

theorem Multiset.subset_add_right {α : Type u_1} {s t : Multiset α} : s ⊆ t + s

theorem Multiset.le_iff_exists_add {α : Type u_1} {s t : Multiset α} : s ≤ t ↔ ∃ (u : Multiset α), t = s + u

@[simp]

theorem Multiset.cons_add {α : Type u_1} (a : α) (s t : Multiset α) : a ::ₘ s + t = a ::ₘ (s + t)

@[simp]

theorem Multiset.add_cons {α : Type u_1} (a : α) (s t : Multiset α) : s + a ::ₘ t = a ::ₘ (s + t)

@[simp]

theorem Multiset.mem_add {α : Type u_1} {a : α} {s t : Multiset α} : a ∈ s + t ↔ a ∈ s ∨ a ∈ t

Cardinality

def Multiset.card {α : Type u_1} : Multiset α → ℕ

The cardinality of a multiset is the sum of the multiplicities of all its elements, or simply the length of the underlying list.

Equations

• Multiset.card = Quot.lift List.length ⋯

@[simp]

theorem Multiset.coe_card {α : Type u_1} (l : List α) : (↑l).card = l.length

@[simp]

theorem Multiset.length_toList {α : Type u_1} (s : Multiset α) : s.toList.length = s.card

@[simp]

theorem Multiset.card_zero {α : Type u_1} : card 0 = 0

@[simp]

theorem Multiset.card_add {α : Type u_1} (s t : Multiset α) : (s + t).card = s.card + t.card

@[simp]

theorem Multiset.card_cons {α : Type u_1} (a : α) (s : Multiset α) : (a ::ₘ s).card = s.card + 1

@[simp]

theorem Multiset.card_singleton {α : Type u_1} (a : α) : {a}.card = 1

theorem Multiset.card_pair {α : Type u_1} (a b : α) : {a, b}.card = 2

theorem Multiset.card_eq_one {α : Type u_1} {s : Multiset α} : s.card = 1 ↔ ∃ (a : α), s = {a}

theorem Multiset.card_le_card {α : Type u_1} {s t : Multiset α} (h : s ≤ t) : s.card ≤ t.card

theorem Multiset.card_mono {α : Type u_1} : Monotone card

theorem Multiset.eq_of_le_of_card_le {α : Type u_1} {s t : Multiset α} (h : s ≤ t) : t.card ≤ s.card → s = t

theorem Multiset.card_lt_card {α : Type u_1} {s t : Multiset α} (h : s < t) : s.card < t.card

theorem Multiset.card_strictMono {α : Type u_1} : StrictMono card

theorem Multiset.lt_iff_cons_le {α : Type u_1} {s t : Multiset α} : s < t ↔ ∃ (a : α), a ::ₘ s ≤ t

@[simp]

theorem Multiset.card_eq_zero {α : Type u_1} {s : Multiset α} : s.card = 0 ↔ s = 0

theorem Multiset.card_pos {α : Type u_1} {s : Multiset α} : 0 < s.card ↔ s ≠ 0

theorem Multiset.card_pos_iff_exists_mem {α : Type u_1} {s : Multiset α} : 0 < s.card ↔ ∃ (a : α), a ∈ s

theorem Multiset.card_eq_two {α : Type u_1} {s : Multiset α} : s.card = 2 ↔ ∃ (x : α) (y : α), s = {x, y}

theorem Multiset.card_eq_three {α : Type u_1} {s : Multiset α} : s.card = 3 ↔ ∃ (x : α) (y : α) (z : α), s = {x, y, z}

Induction principles

@[irreducible]

def Multiset.strongInductionOn {α : Type u_1} {p : Multiset α → Sort u_3} (s : Multiset α) (ih : (s : Multiset α) → ((t : Multiset α) → t < s → p t) → p s) : p s

The strong induction principle for multisets.

Equations

• s.strongInductionOn ih = ih s fun (t : Multiset α) (_h : t < s) => t.strongInductionOn ih

theorem Multiset.strongInductionOn_eq {α : Type u_1} {p : Multiset α → Sort u_3} (s : Multiset α) (H : (s : Multiset α) → ((t : Multiset α) → t < s → p t) → p s) : s.strongInductionOn H = H s fun (t : Multiset α) (_h : t < s) => t.strongInductionOn H

theorem Multiset.case_strongInductionOn {α : Type u_1} {p : Multiset α → Prop} (s : Multiset α) (h₀ : p 0) (h₁ : ∀ (a : α) (s : Multiset α), (∀ t ≤ s, p t) → p (a ::ₘ s)) : p s

@[irreducible]

def Multiset.strongDownwardInduction {α : Type u_1} {p : Multiset α → Sort u_3} {n : ℕ} (H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁) (s : Multiset α) : s.card ≤ n → p s

Suppose that, given that p t can be defined on all supersets of s of cardinality less than n, one knows how to define p s. Then one can inductively define p s for all multisets s of cardinality less than n, starting from multisets of card n and iterating. This can be used either to define data, or to prove properties.

Equations

• Multiset.strongDownwardInduction H s = H s fun {t : Multiset α} (ht : t.card ≤ n) (_h : s < t) => Multiset.strongDownwardInduction H t ht

theorem Multiset.strongDownwardInduction_eq {α : Type u_1} {p : Multiset α → Sort u_3} {n : ℕ} (H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁) (s : Multiset α) : strongDownwardInduction H s = H s fun {t₂ : Multiset α} (ht : t₂.card ≤ n) (_hst : s < t₂) => strongDownwardInduction H t₂ ht

def Multiset.strongDownwardInductionOn {α : Type u_1} {p : Multiset α → Sort u_3} {n : ℕ} (s : Multiset α) : ((t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁) → s.card ≤ n → p s

Analogue of strongDownwardInduction with order of arguments swapped.

Equations

• s.strongDownwardInductionOn H = Multiset.strongDownwardInduction H s

theorem Multiset.strongDownwardInductionOn_eq {α : Type u_1} {p : Multiset α → Sort u_3} (s : Multiset α) {n : ℕ} (H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁) : (fun (a : s.card ≤ n) => s.strongDownwardInductionOn H a) = H s fun {t : Multiset α} (ht : t.card ≤ n) (_h : s < t) => t.strongDownwardInductionOn H ht

instance Multiset.instWellFoundedLT {α : Type u_1} : WellFoundedLT (Multiset α)

Another way of expressing strongInductionOn: the (<) relation is well-founded.

Multiset.replicate

def Multiset.replicate {α : Type u_1} (n : ℕ) (a : α) : Multiset α

replicate n a is the multiset containing only a with multiplicity n.

Equations

• Multiset.replicate n a = ↑(List.replicate n a)

theorem Multiset.coe_replicate {α : Type u_1} (n : ℕ) (a : α) : ↑(List.replicate n a) = replicate n a

@[simp]

theorem Multiset.replicate_zero {α : Type u_1} (a : α) : replicate 0 a = 0

@[simp]

theorem Multiset.replicate_succ {α : Type u_1} (a : α) (n : ℕ) : replicate (n + 1) a = a ::ₘ replicate n a

theorem Multiset.replicate_add {α : Type u_1} (m n : ℕ) (a : α) : replicate (m + n) a = replicate m a + replicate n a

theorem Multiset.replicate_one {α : Type u_1} (a : α) : replicate 1 a = {a}

@[simp]

theorem Multiset.card_replicate {α : Type u_1} (n : ℕ) (a : α) : (replicate n a).card = n

theorem Multiset.mem_replicate {α : Type u_1} {a b : α} {n : ℕ} : b ∈ replicate n a ↔ n ≠ 0 ∧ b = a

theorem Multiset.eq_of_mem_replicate {α : Type u_1} {a b : α} {n : ℕ} : b ∈ replicate n a → b = a

theorem Multiset.eq_replicate_card {α : Type u_1} {a : α} {s : Multiset α} : s = replicate s.card a ↔ ∀ b ∈ s, b = a

theorem Multiset.eq_replicate_of_mem {α : Type u_1} {a : α} {s : Multiset α} : (∀ b ∈ s, b = a) → s = replicate s.card a

Alias of the reverse direction of Multiset.eq_replicate_card.

theorem Multiset.eq_replicate {α : Type u_1} {a : α} {n : ℕ} {s : Multiset α} : s = replicate n a ↔ s.card = n ∧ ∀ b ∈ s, b = a

theorem Multiset.replicate_right_injective {α : Type u_1} {n : ℕ} (hn : n ≠ 0) : Function.Injective (replicate n)

@[simp]

theorem Multiset.replicate_right_inj {α : Type u_1} {a b : α} {n : ℕ} (h : n ≠ 0) : replicate n a = replicate n b ↔ a = b

theorem Multiset.replicate_left_injective {α : Type u_1} (a : α) : Function.Injective fun (x : ℕ) => replicate x a

theorem Multiset.replicate_subset_singleton {α : Type u_1} (n : ℕ) (a : α) : replicate n a ⊆ {a}

theorem Multiset.replicate_le_coe {α : Type u_1} {a : α} {n : ℕ} {l : List α} : replicate n a ≤ ↑l ↔ (List.replicate n a).Sublist l

theorem Multiset.replicate_le_replicate {α : Type u_1} (a : α) {k n : ℕ} : replicate k a ≤ replicate n a ↔ k ≤ n

theorem Multiset.replicate_mono {α : Type u_1} (a : α) {k n : ℕ} (h : k ≤ n) : replicate k a ≤ replicate n a

theorem Multiset.le_replicate_iff {α : Type u_1} {m : Multiset α} {a : α} {n : ℕ} : m ≤ replicate n a ↔ ∃ k ≤ n, m = replicate k a

theorem Multiset.lt_replicate_succ {α : Type u_1} {m : Multiset α} {x : α} {n : ℕ} : m < replicate (n + 1) x ↔ m ≤ replicate n x

Erasing one copy of an element

def Multiset.erase {α : Type u_1} [DecidableEq α] (s : Multiset α) (a : α) : Multiset α

erase s a is the multiset that subtracts 1 from the multiplicity of a.

Equations

• s.erase a = Quot.liftOn s (fun (l : List α) => ↑(l.erase a)) ⋯

@[simp]

theorem Multiset.coe_erase {α : Type u_1} [DecidableEq α] (l : List α) (a : α) : (↑l).erase a = ↑(l.erase a)

@[simp]

theorem Multiset.erase_zero {α : Type u_1} [DecidableEq α] (a : α) : erase 0 a = 0

@[simp]

theorem Multiset.erase_cons_head {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) : (a ::ₘ s).erase a = s

@[simp]

theorem Multiset.erase_cons_tail {α : Type u_1} [DecidableEq α] {a b : α} (s : Multiset α) (h : b ≠ a) : (b ::ₘ s).erase a = b ::ₘ s.erase a

@[simp]

theorem Multiset.erase_singleton {α : Type u_1} [DecidableEq α] (a : α) : {a}.erase a = 0

@[simp]

theorem Multiset.erase_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} : a ∉ s → s.erase a = s

@[simp]

theorem Multiset.cons_erase {α : Type u_1} [DecidableEq α] {s : Multiset α} {a : α} : a ∈ s → a ::ₘ s.erase a = s

theorem Multiset.erase_cons_tail_of_mem {α : Type u_1} [DecidableEq α] {s : Multiset α} {a b : α} (h : a ∈ s) : (b ::ₘ s).erase a = b ::ₘ s.erase a

theorem Multiset.le_cons_erase {α : Type u_1} [DecidableEq α] (s : Multiset α) (a : α) : s ≤ a ::ₘ s.erase a

theorem Multiset.add_singleton_eq_iff {α : Type u_1} [DecidableEq α] {s t : Multiset α} {a : α} : s + {a} = t ↔ a ∈ t ∧ s = t.erase a

theorem Multiset.erase_add_left_pos {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} (t : Multiset α) : a ∈ s → (s + t).erase a = s.erase a + t

theorem Multiset.erase_add_right_pos {α : Type u_1} [DecidableEq α] {t : Multiset α} {a : α} (s : Multiset α) (h : a ∈ t) : (s + t).erase a = s + t.erase a

theorem Multiset.erase_add_right_neg {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} (t : Multiset α) : a ∉ s → (s + t).erase a = s + t.erase a

theorem Multiset.erase_add_left_neg {α : Type u_1} [DecidableEq α] {t : Multiset α} {a : α} (s : Multiset α) (h : a ∉ t) : (s + t).erase a = s.erase a + t

theorem Multiset.erase_le {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) : s.erase a ≤ s

@[simp]

theorem Multiset.erase_lt {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} : s.erase a < s ↔ a ∈ s

theorem Multiset.erase_subset {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) : s.erase a ⊆ s

theorem Multiset.mem_erase_of_ne {α : Type u_1} [DecidableEq α] {a b : α} {s : Multiset α} (ab : a ≠ b) : a ∈ s.erase b ↔ a ∈ s

theorem Multiset.mem_of_mem_erase {α : Type u_1} [DecidableEq α] {a b : α} {s : Multiset α} : a ∈ s.erase b → a ∈ s

theorem Multiset.erase_comm {α : Type u_1} [DecidableEq α] (s : Multiset α) (a b : α) : (s.erase a).erase b = (s.erase b).erase a

instance Multiset.instRightCommutativeErase {α : Type u_1} [DecidableEq α] : RightCommutative erase

theorem Multiset.erase_le_erase {α : Type u_1} [DecidableEq α] {s t : Multiset α} (a : α) (h : s ≤ t) : s.erase a ≤ t.erase a

theorem Multiset.erase_le_iff_le_cons {α : Type u_1} [DecidableEq α] {s t : Multiset α} {a : α} : s.erase a ≤ t ↔ s ≤ a ::ₘ t

@[simp]

theorem Multiset.card_erase_of_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} : a ∈ s → (s.erase a).card = s.card.pred

@[simp]

theorem Multiset.card_erase_add_one {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} : a ∈ s → (s.erase a).card + 1 = s.card

theorem Multiset.card_erase_lt_of_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} : a ∈ s → (s.erase a).card < s.card

theorem Multiset.card_erase_le {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} : (s.erase a).card ≤ s.card

theorem Multiset.card_erase_eq_ite {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} : (s.erase a).card = if a ∈ s then s.card.pred else s.card

@[simp]

theorem Multiset.coe_reverse {α : Type u_1} (l : List α) : ↑l.reverse = ↑l

Multiset.map

def Multiset.map {α : Type u_1} {β : Type v} (f : α → β) (s : Multiset α) : Multiset β

map f s is the lift of the list map operation. The multiplicity of b in map f s is the number of a ∈ s (counting multiplicity) such that f a = b.

Equations

• Multiset.map f s = Quot.liftOn s (fun (l : List α) => ↑(List.map f l)) ⋯

theorem Multiset.map_congr {α : Type u_1} {β : Type v} {f g : α → β} {s t : Multiset α} : s = t → (∀ x ∈ t, f x = g x) → map f s = map g t

theorem Multiset.map_hcongr {α : Type u_1} {β β' : Type v} {m : Multiset α} {f : α → β} {f' : α → β'} (h : β = β') (hf : ∀ a ∈ m, HEq (f a) (f' a)) : HEq (map f m) (map f' m)

theorem Multiset.forall_mem_map_iff {α : Type u_1} {β : Type v} {f : α → β} {p : β → Prop} {s : Multiset α} : (∀ y ∈ map f s, p y) ↔ ∀ x ∈ s, p (f x)

@[simp]

theorem Multiset.map_coe {α : Type u_1} {β : Type v} (f : α → β) (l : List α) : map f ↑l = ↑(List.map f l)

@[simp]

theorem Multiset.map_zero {α : Type u_1} {β : Type v} (f : α → β) : map f 0 = 0

@[simp]

theorem Multiset.map_cons {α : Type u_1} {β : Type v} (f : α → β) (a : α) (s : Multiset α) : map f (a ::ₘ s) = f a ::ₘ map f s

theorem Multiset.map_comp_cons {α : Type u_1} {β : Type v} (f : α → β) (t : α) : map f ∘ cons t = cons (f t) ∘ map f

@[simp]

theorem Multiset.map_singleton {α : Type u_1} {β : Type v} (f : α → β) (a : α) : map f {a} = {f a}

@[simp]

theorem Multiset.map_replicate {α : Type u_1} {β : Type v} (f : α → β) (k : ℕ) (a : α) : map f (replicate k a) = replicate k (f a)

@[simp]

theorem Multiset.map_add {α : Type u_1} {β : Type v} (f : α → β) (s t : Multiset α) : map f (s + t) = map f s + map f t

instance Multiset.canLift {α : Type u_1} {β : Type v} (c : β → α) (p : α → Prop) [CanLift α β c p] : CanLift (Multiset α) (Multiset β) (map c) fun (s : Multiset α) => ∀ x ∈ s, p x

If each element of s : Multiset α can be lifted to β, then s can be lifted to Multiset β.

@[simp]

theorem Multiset.mem_map {α : Type u_1} {β : Type v} {f : α → β} {b : β} {s : Multiset α} : b ∈ map f s ↔ ∃ a ∈ s, f a = b

@[simp]

theorem Multiset.card_map {α : Type u_1} {β : Type v} (f : α → β) (s : Multiset α) : (map f s).card = s.card

@[simp]

theorem Multiset.map_eq_zero {α : Type u_1} {β : Type v} {s : Multiset α} {f : α → β} : map f s = 0 ↔ s = 0

theorem Multiset.mem_map_of_mem {α : Type u_1} {β : Type v} (f : α → β) {a : α} {s : Multiset α} (h : a ∈ s) : f a ∈ map f s

theorem Multiset.map_eq_singleton {α : Type u_1} {β : Type v} {f : α → β} {s : Multiset α} {b : β} : map f s = {b} ↔ ∃ (a : α), s = {a} ∧ f a = b

theorem Multiset.map_eq_cons {α : Type u_1} {β : Type v} [DecidableEq α] (f : α → β) (s : Multiset α) (t : Multiset β) (b : β) : (∃ a ∈ s, f a = b ∧ map f (s.erase a) = t) ↔ map f s = b ::ₘ t

@[simp]

theorem Multiset.mem_map_of_injective {α : Type u_1} {β : Type v} {f : α → β} (H : Function.Injective f) {a : α} {s : Multiset α} : f a ∈ map f s ↔ a ∈ s

@[simp]

theorem Multiset.map_map {α : Type u_1} {β : Type v} {γ : Type u_2} (g : β → γ) (f : α → β) (s : Multiset α) : map g (map f s) = map (g ∘ f) s

theorem Multiset.map_id {α : Type u_1} (s : Multiset α) : map id s = s

@[simp]

theorem Multiset.map_id' {α : Type u_1} (s : Multiset α) : map (fun (x : α) => x) s = s

theorem Multiset.map_const {α : Type u_1} {β : Type v} (s : Multiset α) (b : β) : map (Function.const α b) s = replicate s.card b

@[simp]

theorem Multiset.map_const' {α : Type u_1} {β : Type v} (s : Multiset α) (b : β) : map (fun (x : α) => b) s = replicate s.card b

theorem Multiset.eq_of_mem_map_const {α : Type u_1} {β : Type v} {b₁ b₂ : β} {l : List α} (h : b₁ ∈ map (Function.const α b₂) ↑l) : b₁ = b₂

@[simp]

theorem Multiset.map_le_map {α : Type u_1} {β : Type v} {f : α → β} {s t : Multiset α} (h : s ≤ t) : map f s ≤ map f t

@[simp]

theorem Multiset.map_lt_map {α : Type u_1} {β : Type v} {f : α → β} {s t : Multiset α} (h : s < t) : map f s < map f t

theorem Multiset.map_mono {α : Type u_1} {β : Type v} (f : α → β) : Monotone (map f)

theorem Multiset.map_strictMono {α : Type u_1} {β : Type v} (f : α → β) : StrictMono (map f)

@[simp]

theorem Multiset.map_subset_map {α : Type u_1} {β : Type v} {f : α → β} {s t : Multiset α} (H : s ⊆ t) : map f s ⊆ map f t

theorem Multiset.map_erase {α : Type u_1} {β : Type v} [DecidableEq α] [DecidableEq β] (f : α → β) (hf : Function.Injective f) (x : α) (s : Multiset α) : map f (s.erase x) = (map f s).erase (f x)

theorem Multiset.map_erase_of_mem {α : Type u_1} {β : Type v} [DecidableEq α] [DecidableEq β] (f : α → β) (s : Multiset α) {x : α} (h : x ∈ s) : map f (s.erase x) = (map f s).erase (f x)

theorem Multiset.map_surjective_of_surjective {α : Type u_1} {β : Type v} {f : α → β} (hf : Function.Surjective f) : Function.Surjective (map f)

Multiset.fold

def Multiset.foldl {α : Type u_1} {β : Type v} (f : β → α → β) [RightCommutative f] (b : β) (s : Multiset α) : β

foldl f H b s is the lift of the list operation foldl f b l, which folds f over the multiset. It is well defined when f is right-commutative, that is, f (f b a₁) a₂ = f (f b a₂) a₁.

Equations

• Multiset.foldl f b s = Quot.liftOn s (fun (l : List α) => List.foldl f b l) ⋯

@[simp]

theorem Multiset.foldl_zero {α : Type u_1} {β : Type v} (f : β → α → β) [RightCommutative f] (b : β) : foldl f b 0 = b

@[simp]

theorem Multiset.foldl_cons {α : Type u_1} {β : Type v} (f : β → α → β) [RightCommutative f] (b : β) (a : α) (s : Multiset α) : foldl f b (a ::ₘ s) = foldl f (f b a) s

@[simp]

theorem Multiset.foldl_add {α : Type u_1} {β : Type v} (f : β → α → β) [RightCommutative f] (b : β) (s t : Multiset α) : foldl f b (s + t) = foldl f (foldl f b s) t

def Multiset.foldr {α : Type u_1} {β : Type v} (f : α → β → β) [LeftCommutative f] (b : β) (s : Multiset α) : β

foldr f H b s is the lift of the list operation foldr f b l, which folds f over the multiset. It is well defined when f is left-commutative, that is, f a₁ (f a₂ b) = f a₂ (f a₁ b).

Equations

• Multiset.foldr f b s = Quot.liftOn s (fun (l : List α) => List.foldr f b l) ⋯

@[simp]

theorem Multiset.foldr_zero {α : Type u_1} {β : Type v} (f : α → β → β) [LeftCommutative f] (b : β) : foldr f b 0 = b

@[simp]

theorem Multiset.foldr_cons {α : Type u_1} {β : Type v} (f : α → β → β) [LeftCommutative f] (b : β) (a : α) (s : Multiset α) : foldr f b (a ::ₘ s) = f a (foldr f b s)

@[simp]

theorem Multiset.foldr_singleton {α : Type u_1} {β : Type v} (f : α → β → β) [LeftCommutative f] (b : β) (a : α) : foldr f b {a} = f a b

@[simp]

theorem Multiset.foldr_add {α : Type u_1} {β : Type v} (f : α → β → β) [LeftCommutative f] (b : β) (s t : Multiset α) : foldr f b (s + t) = foldr f (foldr f b t) s

@[simp]

theorem Multiset.coe_foldr {α : Type u_1} {β : Type v} (f : α → β → β) [LeftCommutative f] (b : β) (l : List α) : foldr f b ↑l = List.foldr f b l

@[simp]

theorem Multiset.coe_foldl {α : Type u_1} {β : Type v} (f : β → α → β) [RightCommutative f] (b : β) (l : List α) : foldl f b ↑l = List.foldl f b l

theorem Multiset.coe_foldr_swap {α : Type u_1} {β : Type v} (f : α → β → β) [LeftCommutative f] (b : β) (l : List α) : foldr f b ↑l = List.foldl (fun (x : β) (y : α) => f y x) b l

theorem Multiset.foldr_swap {α : Type u_1} {β : Type v} (f : α → β → β) [LeftCommutative f] (b : β) (s : Multiset α) : foldr f b s = foldl (fun (x : β) (y : α) => f y x) b s

theorem Multiset.foldl_swap {α : Type u_1} {β : Type v} (f : β → α → β) [RightCommutative f] (b : β) (s : Multiset α) : foldl f b s = foldr (fun (x : α) (y : β) => f y x) b s

theorem Multiset.foldr_induction' {α : Type u_1} {β : Type v} (f : α → β → β) [LeftCommutative f] (x : β) (q : α → Prop) (p : β → Prop) (s : Multiset α) (hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)) (px : p x) (q_s : ∀ a ∈ s, q a) : p (foldr f x s)

theorem Multiset.foldr_induction {α : Type u_1} (f : α → α → α) [LeftCommutative f] (x : α) (p : α → Prop) (s : Multiset α) (p_f : ∀ (a b : α), p a → p b → p (f a b)) (px : p x) (p_s : ∀ a ∈ s, p a) : p (foldr f x s)

theorem Multiset.foldl_induction' {α : Type u_1} {β : Type v} (f : β → α → β) [RightCommutative f] (x : β) (q : α → Prop) (p : β → Prop) (s : Multiset α) (hpqf : ∀ (a : α) (b : β), q a → p b → p (f b a)) (px : p x) (q_s : ∀ a ∈ s, q a) : p (foldl f x s)

theorem Multiset.foldl_induction {α : Type u_1} (f : α → α → α) [RightCommutative f] (x : α) (p : α → Prop) (s : Multiset α) (p_f : ∀ (a b : α), p a → p b → p (f b a)) (px : p x) (p_s : ∀ a ∈ s, p a) : p (foldl f x s)

Map for partial functions

def Multiset.pmap {α : Type u_1} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) (s : Multiset α) : (∀ a ∈ s, p a) → Multiset β

Lift of the list pmap operation. Map a partial function f over a multiset s whose elements are all in the domain of f.

Equations

• Multiset.pmap f s = Quot.recOn (motive := fun (x : Multiset α) => (∀ a ∈ x, p a) → Multiset β) s (fun (l : List α) (H : ∀ a ∈ Quot.mk (⇑(List.isSetoid α)) l, p a) => ↑(List.pmap f l H)) ⋯

@[simp]

theorem Multiset.coe_pmap {α : Type u_1} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) (l : List α) (H : ∀ a ∈ l, p a) : pmap f (↑l) H = ↑(List.pmap f l H)

@[simp]

theorem Multiset.pmap_zero {α : Type u_1} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) (h : ∀ a ∈ 0, p a) : pmap f 0 h = 0

@[simp]

theorem Multiset.pmap_cons {α : Type u_1} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) (a : α) (m : Multiset α) (h : ∀ b ∈ a ::ₘ m, p b) : pmap f (a ::ₘ m) h = f a ⋯ ::ₘ pmap f m ⋯

def Multiset.attach {α : Type u_1} (s : Multiset α) : Multiset { x : α // x ∈ s }

"Attach" a proof that a ∈ s to each element a in s to produce a multiset on {x // x ∈ s}.

Equations

• s.attach = Multiset.pmap Subtype.mk s ⋯

@[simp]

theorem Multiset.coe_attach {α : Type u_1} (l : List α) : (↑l).attach = ↑l.attach

theorem Multiset.sizeOf_lt_sizeOf_of_mem {α : Type u_1} [SizeOf α] {x : α} {s : Multiset α} (hx : x ∈ s) : sizeOf x < sizeOf s

theorem Multiset.pmap_eq_map {α : Type u_1} {β : Type v} (p : α → Prop) (f : α → β) (s : Multiset α) (H : ∀ a ∈ s, p a) : pmap (fun (a : α) (x : p a) => f a) s H = map f s

theorem Multiset.pmap_congr {α : Type u_1} {β : Type v} {p q : α → Prop} {f : (a : α) → p a → β} {g : (a : α) → q a → β} (s : Multiset α) {H₁ : ∀ a ∈ s, p a} {H₂ : ∀ a ∈ s, q a} : (∀ a ∈ s, ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂) → pmap f s H₁ = pmap g s H₂

theorem Multiset.map_pmap {α : Type u_1} {β : Type v} {γ : Type u_2} {p : α → Prop} (g : β → γ) (f : (a : α) → p a → β) (s : Multiset α) (H : ∀ a ∈ s, p a) : map g (pmap f s H) = pmap (fun (a : α) (h : p a) => g (f a h)) s H

theorem Multiset.pmap_eq_map_attach {α : Type u_1} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) (s : Multiset α) (H : ∀ a ∈ s, p a) : pmap f s H = map (fun (x : { x : α // x ∈ s }) => f ↑x ⋯) s.attach

theorem Multiset.attach_map_val' {α : Type u_1} {β : Type v} (s : Multiset α) (f : α → β) : map (fun (i : { x : α // x ∈ s }) => f ↑i) s.attach = map f s

@[simp]

theorem Multiset.attach_map_val {α : Type u_1} (s : Multiset α) : map Subtype.val s.attach = s

@[simp]

theorem Multiset.mem_attach {α : Type u_1} (s : Multiset α) (x : { x : α // x ∈ s }) : x ∈ s.attach

@[simp]

theorem Multiset.mem_pmap {α : Type u_1} {β : Type v} {p : α → Prop} {f : (a : α) → p a → β} {s : Multiset α} {H : ∀ a ∈ s, p a} {b : β} : b ∈ pmap f s H ↔ ∃ (a : α) (h : a ∈ s), f a ⋯ = b

@[simp]

theorem Multiset.card_pmap {α : Type u_1} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) (s : Multiset α) (H : ∀ a ∈ s, p a) : (pmap f s H).card = s.card

@[simp]

theorem Multiset.card_attach {α : Type u_1} {m : Multiset α} : m.attach.card = m.card

@[simp]

theorem Multiset.attach_zero {α : Type u_1} : attach 0 = 0

theorem Multiset.attach_cons {α : Type u_1} (a : α) (m : Multiset α) : (a ::ₘ m).attach = ⟨a, ⋯⟩ ::ₘ map (fun (p : { x : α // x ∈ m }) => ⟨↑p, ⋯⟩) m.attach

def Multiset.decidableForallMultiset {α : Type u_1} {m : Multiset α} {p : α → Prop} [(a : α) → Decidable (p a)] : Decidable (∀ a ∈ m, p a)

If p is a decidable predicate, so is the predicate that all elements of a multiset satisfy p.

Equations

• Multiset.decidableForallMultiset = Quotient.recOnSubsingleton m fun (l : List α) => decidable_of_iff (∀ a ∈ l, p a) ⋯

instance Multiset.decidableDforallMultiset {α : Type u_1} {m : Multiset α} {p : (a : α) → a ∈ m → Prop} [_hp : (a : α) → (h : a ∈ m) → Decidable (p a h)] : Decidable (∀ (a : α) (h : a ∈ m), p a h)

Equations

• Multiset.decidableDforallMultiset = decidable_of_iff (∀ a ∈ m.attach, p ↑a ⋯) ⋯

instance Multiset.decidableEqPiMultiset {α : Type u_1} {m : Multiset α} {β : α → Type u_3} [(a : α) → DecidableEq (β a)] : DecidableEq ((a : α) → a ∈ m → β a)

decidable equality for functions whose domain is bounded by multisets

Equations

• Multiset.decidableEqPiMultiset f g = decidable_of_iff (∀ (a : α) (h : a ∈ m), f a h = g a h) ⋯

def Multiset.decidableExistsMultiset {α : Type u_1} {m : Multiset α} {p : α → Prop} [DecidablePred p] : Decidable (∃ x ∈ m, p x)

If p is a decidable predicate, so is the existence of an element in a multiset satisfying p.

Equations

• Multiset.decidableExistsMultiset = Quotient.recOnSubsingleton m fun (l : List α) => decidable_of_iff (∃ a ∈ l, p a) ⋯

instance Multiset.decidableDexistsMultiset {α : Type u_1} {m : Multiset α} {p : (a : α) → a ∈ m → Prop} [_hp : (a : α) → (h : a ∈ m) → Decidable (p a h)] : Decidable (∃ (a : α) (h : a ∈ m), p a h)

Equations

• Multiset.decidableDexistsMultiset = decidable_of_iff (∃ x ∈ m.attach, p ↑x ⋯) ⋯

Multiset.filter

def Multiset.filter {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Multiset α) : Multiset α

Filter p s returns the elements in s (with the same multiplicities) which satisfy p, and removes the rest.

Equations

• Multiset.filter p s = Quot.liftOn s (fun (l : List α) => ↑(List.filter (fun (b : α) => decide (p b)) l)) ⋯

@[simp]

theorem Multiset.filter_coe {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : List α) : filter p ↑l = ↑(List.filter (fun (b : α) => decide (p b)) l)

@[simp]

theorem Multiset.filter_zero {α : Type u_1} (p : α → Prop) [DecidablePred p] : filter p 0 = 0

theorem Multiset.filter_congr {α : Type u_1} {p q : α → Prop} [DecidablePred p] [DecidablePred q] {s : Multiset α} : (∀ x ∈ s, p x ↔ q x) → filter p s = filter q s

@[simp]

theorem Multiset.filter_add {α : Type u_1} (p : α → Prop) [DecidablePred p] (s t : Multiset α) : filter p (s + t) = filter p s + filter p t

@[simp]

theorem Multiset.filter_le {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Multiset α) : filter p s ≤ s

@[simp]

theorem Multiset.filter_subset {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Multiset α) : filter p s ⊆ s

theorem Multiset.filter_le_filter {α : Type u_1} (p : α → Prop) [DecidablePred p] {s t : Multiset α} (h : s ≤ t) : filter p s ≤ filter p t

theorem Multiset.monotone_filter_left {α : Type u_1} (p : α → Prop) [DecidablePred p] : Monotone (filter p)

theorem Multiset.monotone_filter_right {α : Type u_1} (s : Multiset α) ⦃p q : α → Prop⦄ [DecidablePred p] [DecidablePred q] (h : ∀ (b : α), p b → q b) : filter p s ≤ filter q s

@[simp]

theorem Multiset.filter_cons_of_pos {α : Type u_1} {p : α → Prop} [DecidablePred p] {a : α} (s : Multiset α) : p a → filter p (a ::ₘ s) = a ::ₘ filter p s

@[simp]

theorem Multiset.filter_cons_of_neg {α : Type u_1} {p : α → Prop} [DecidablePred p] {a : α} (s : Multiset α) : ¬p a → filter p (a ::ₘ s) = filter p s

@[simp]

theorem Multiset.mem_filter {α : Type u_1} {p : α → Prop} [DecidablePred p] {a : α} {s : Multiset α} : a ∈ filter p s ↔ a ∈ s ∧ p a

theorem Multiset.of_mem_filter {α : Type u_1} {p : α → Prop} [DecidablePred p] {a : α} {s : Multiset α} (h : a ∈ filter p s) : p a

theorem Multiset.mem_of_mem_filter {α : Type u_1} {p : α → Prop} [DecidablePred p] {a : α} {s : Multiset α} (h : a ∈ filter p s) : a ∈ s

theorem Multiset.mem_filter_of_mem {α : Type u_1} {p : α → Prop} [DecidablePred p] {a : α} {l : Multiset α} (m : a ∈ l) (h : p a) : a ∈ filter p l

theorem Multiset.filter_eq_self {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Multiset α} : filter p s = s ↔ ∀ a ∈ s, p a

theorem Multiset.filter_eq_nil {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Multiset α} : filter p s = 0 ↔ ∀ a ∈ s, ¬p a

theorem Multiset.le_filter {α : Type u_1} {p : α → Prop} [DecidablePred p] {s t : Multiset α} : s ≤ filter p t ↔ s ≤ t ∧ ∀ a ∈ s, p a

theorem Multiset.filter_cons {α : Type u_1} {p : α → Prop} [DecidablePred p] {a : α} (s : Multiset α) : filter p (a ::ₘ s) = (if p a then {a} else 0) + filter p s

theorem Multiset.filter_singleton {α : Type u_1} {a : α} (p : α → Prop) [DecidablePred p] : filter p {a} = if p a then {a} else ∅

@[simp]

theorem Multiset.filter_filter {α : Type u_1} (p : α → Prop) [DecidablePred p] (q : α → Prop) [DecidablePred q] (s : Multiset α) : filter p (filter q s) = filter (fun (a : α) => p a ∧ q a) s

theorem Multiset.filter_comm {α : Type u_1} (p : α → Prop) [DecidablePred p] (q : α → Prop) [DecidablePred q] (s : Multiset α) : filter p (filter q s) = filter q (filter p s)

theorem Multiset.filter_add_filter {α : Type u_1} (p : α → Prop) [DecidablePred p] (q : α → Prop) [DecidablePred q] (s : Multiset α) : filter p s + filter q s = filter (fun (a : α) => p a ∨ q a) s + filter (fun (a : α) => p a ∧ q a) s

theorem Multiset.filter_add_not {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Multiset α) : filter p s + filter (fun (a : α) => ¬p a) s = s

theorem Multiset.filter_map {α : Type u_1} {β : Type v} (p : α → Prop) [DecidablePred p] (f : β → α) (s : Multiset β) : filter p (map f s) = map f (filter (p ∘ f) s)

theorem Multiset.map_filter' {α : Type u_1} {β : Type v} (p : α → Prop) [DecidablePred p] {f : α → β} (hf : Function.Injective f) (s : Multiset α) [DecidablePred fun (b : β) => ∃ (a : α), p a ∧ f a = b] : map f (filter p s) = filter (fun (b : β) => ∃ (a : α), p a ∧ f a = b) (map f s)

theorem Multiset.card_filter_le_iff {α : Type u_1} (s : Multiset α) (P : α → Prop) [DecidablePred P] (n : ℕ) : (filter P s).card ≤ n ↔ ∀ s' ≤ s, n < s'.card → ∃ a ∈ s', ¬P a

Simultaneously filter and map elements of a multiset

def Multiset.filterMap {α : Type u_1} {β : Type v} (f : α → Option β) (s : Multiset α) : Multiset β

filterMap f s is a combination filter/map operation on s. The function f : α → Option β is applied to each element of s; if f a is some b then b is added to the result, otherwise a is removed from the resulting multiset.

Equations

• Multiset.filterMap f s = Quot.liftOn s (fun (l : List α) => ↑(List.filterMap f l)) ⋯

@[simp]

theorem Multiset.filterMap_coe {α : Type u_1} {β : Type v} (f : α → Option β) (l : List α) : filterMap f ↑l = ↑(List.filterMap f l)

@[simp]

theorem Multiset.filterMap_zero {α : Type u_1} {β : Type v} (f : α → Option β) : filterMap f 0 = 0

@[simp]

theorem Multiset.filterMap_cons_none {α : Type u_1} {β : Type v} {f : α → Option β} (a : α) (s : Multiset α) (h : f a = none) : filterMap f (a ::ₘ s) = filterMap f s

@[simp]

theorem Multiset.filterMap_cons_some {α : Type u_1} {β : Type v} (f : α → Option β) (a : α) (s : Multiset α) {b : β} (h : f a = some b) : filterMap f (a ::ₘ s) = b ::ₘ filterMap f s

theorem Multiset.filterMap_eq_map {α : Type u_1} {β : Type v} (f : α → β) : filterMap (some ∘ f) = map f

theorem Multiset.filterMap_eq_filter {α : Type u_1} (p : α → Prop) [DecidablePred p] : filterMap (Option.guard p) = filter p

theorem Multiset.filterMap_filterMap {α : Type u_1} {β : Type v} {γ : Type u_2} (f : α → Option β) (g : β → Option γ) (s : Multiset α) : filterMap g (filterMap f s) = filterMap (fun (x : α) => (f x).bind g) s

theorem Multiset.map_filterMap {α : Type u_1} {β : Type v} {γ : Type u_2} (f : α → Option β) (g : β → γ) (s : Multiset α) : map g (filterMap f s) = filterMap (fun (x : α) => Option.map g (f x)) s

theorem Multiset.filterMap_map {α : Type u_1} {β : Type v} {γ : Type u_2} (f : α → β) (g : β → Option γ) (s : Multiset α) : filterMap g (map f s) = filterMap (g ∘ f) s

theorem Multiset.filter_filterMap {α : Type u_1} {β : Type v} (f : α → Option β) (p : β → Prop) [DecidablePred p] (s : Multiset α) : filter p (filterMap f s) = filterMap (fun (x : α) => Option.filter (fun (b : β) => decide (p b)) (f x)) s

theorem Multiset.filterMap_filter {α : Type u_1} {β : Type v} (p : α → Prop) [DecidablePred p] (f : α → Option β) (s : Multiset α) : filterMap f (filter p s) = filterMap (fun (x : α) => if p x then f x else none) s

@[simp]

theorem Multiset.filterMap_some {α : Type u_1} (s : Multiset α) : filterMap some s = s

@[simp]

theorem Multiset.mem_filterMap {α : Type u_1} {β : Type v} (f : α → Option β) (s : Multiset α) {b : β} : b ∈ filterMap f s ↔ ∃ a ∈ s, f a = some b

theorem Multiset.map_filterMap_of_inv {α : Type u_1} {β : Type v} (f : α → Option β) (g : β → α) (H : ∀ (x : α), Option.map g (f x) = some x) (s : Multiset α) : map g (filterMap f s) = s

theorem Multiset.filterMap_le_filterMap {α : Type u_1} {β : Type v} (f : α → Option β) {s t : Multiset α} (h : s ≤ t) : filterMap f s ≤ filterMap f t

countP

def Multiset.countP {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Multiset α) : ℕ

countP p s counts the number of elements of s (with multiplicity) that satisfy p.

Equations

• Multiset.countP p s = Quot.liftOn s (List.countP fun (b : α) => decide (p b)) ⋯

@[simp]

theorem Multiset.coe_countP {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : List α) : countP p ↑l = List.countP (fun (b : α) => decide (p b)) l

@[simp]

theorem Multiset.countP_zero {α : Type u_1} (p : α → Prop) [DecidablePred p] : countP p 0 = 0

@[simp]

theorem Multiset.countP_cons_of_pos {α : Type u_1} {p : α → Prop} [DecidablePred p] {a : α} (s : Multiset α) : p a → countP p (a ::ₘ s) = countP p s + 1

@[simp]

theorem Multiset.countP_cons_of_neg {α : Type u_1} {p : α → Prop} [DecidablePred p] {a : α} (s : Multiset α) : ¬p a → countP p (a ::ₘ s) = countP p s

theorem Multiset.countP_cons {α : Type u_1} (p : α → Prop) [DecidablePred p] (b : α) (s : Multiset α) : countP p (b ::ₘ s) = countP p s + if p b then 1 else 0

theorem Multiset.countP_eq_card_filter {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Multiset α) : countP p s = (filter p s).card

theorem Multiset.countP_le_card {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Multiset α) : countP p s ≤ s.card

@[simp]

theorem Multiset.countP_add {α : Type u_1} (p : α → Prop) [DecidablePred p] (s t : Multiset α) : countP p (s + t) = countP p s + countP p t

theorem Multiset.card_eq_countP_add_countP {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Multiset α) : s.card = countP p s + countP (fun (x : α) => ¬p x) s

theorem Multiset.countP_le_of_le {α : Type u_1} (p : α → Prop) [DecidablePred p] {s t : Multiset α} (h : s ≤ t) : countP p s ≤ countP p t

@[simp]

theorem Multiset.countP_filter {α : Type u_1} (p : α → Prop) [DecidablePred p] (q : α → Prop) [DecidablePred q] (s : Multiset α) : countP p (filter q s) = countP (fun (a : α) => p a ∧ q a) s

theorem Multiset.countP_eq_countP_filter_add {α : Type u_1} (s : Multiset α) (p q : α → Prop) [DecidablePred p] [DecidablePred q] : countP p s = countP p (filter q s) + countP p (filter (fun (a : α) => ¬q a) s)

@[simp]

theorem Multiset.countP_True {α : Type u_1} {s : Multiset α} : countP (fun (x : α) => True) s = s.card

@[simp]

theorem Multiset.countP_False {α : Type u_1} {s : Multiset α} : countP (fun (x : α) => False) s = 0

theorem Multiset.countP_map {α : Type u_1} {β : Type v} (f : α → β) (s : Multiset α) (p : β → Prop) [DecidablePred p] : countP p (map f s) = (filter (fun (a : α) => p (f a)) s).card

theorem Multiset.countP_attach {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Multiset α) : countP (fun (a : { a : α // a ∈ s }) => p ↑a) s.attach = countP p s

theorem Multiset.filter_attach {α : Type u_1} (s : Multiset α) (p : α → Prop) [DecidablePred p] : filter (fun (a : { a : α // a ∈ s }) => p ↑a) s.attach = map (Subtype.map id ⋯) (filter p s).attach

theorem Multiset.countP_pos {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Multiset α} : 0 < countP p s ↔ ∃ a ∈ s, p a

theorem Multiset.countP_eq_zero {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Multiset α} : countP p s = 0 ↔ ∀ a ∈ s, ¬p a

theorem Multiset.countP_eq_card {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Multiset α} : countP p s = s.card ↔ ∀ a ∈ s, p a

theorem Multiset.countP_pos_of_mem {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Multiset α} {a : α} (h : a ∈ s) (pa : p a) : 0 < countP p s

theorem Multiset.countP_congr {α : Type u_1} {s s' : Multiset α} (hs : s = s') {p p' : α → Prop} [DecidablePred p] [DecidablePred p'] (hp : ∀ x ∈ s, p x = p' x) : countP p s = countP p' s'

Multiplicity of an element

def Multiset.count {α : Type u_1} [DecidableEq α] (a : α) : Multiset α → ℕ

count a s is the multiplicity of a in s.

Equations

• Multiset.count a = Multiset.countP fun (x : α) => a = x

@[simp]

theorem Multiset.coe_count {α : Type u_1} [DecidableEq α] (a : α) (l : List α) : count a ↑l = List.count a l

@[simp]

theorem Multiset.count_zero {α : Type u_1} [DecidableEq α] (a : α) : count a 0 = 0

@[simp]

theorem Multiset.count_cons_self {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) : count a (a ::ₘ s) = count a s + 1

@[simp]

theorem Multiset.count_cons_of_ne {α : Type u_1} [DecidableEq α] {a b : α} (h : a ≠ b) (s : Multiset α) : count a (b ::ₘ s) = count a s

theorem Multiset.count_le_card {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) : count a s ≤ s.card

theorem Multiset.count_le_of_le {α : Type u_1} [DecidableEq α] (a : α) {s t : Multiset α} : s ≤ t → count a s ≤ count a t

theorem Multiset.count_le_count_cons {α : Type u_1} [DecidableEq α] (a b : α) (s : Multiset α) : count a s ≤ count a (b ::ₘ s)

theorem Multiset.count_cons {α : Type u_1} [DecidableEq α] (a b : α) (s : Multiset α) : count a (b ::ₘ s) = count a s + if a = b then 1 else 0

theorem Multiset.count_singleton_self {α : Type u_1} [DecidableEq α] (a : α) : count a {a} = 1

theorem Multiset.count_singleton {α : Type u_1} [DecidableEq α] (a b : α) : count a {b} = if a = b then 1 else 0

@[simp]

theorem Multiset.count_add {α : Type u_1} [DecidableEq α] (a : α) (s t : Multiset α) : count a (s + t) = count a s + count a t

@[simp]

theorem Multiset.count_attach {α : Type u_1} [DecidableEq α] {s : Multiset α} (a : { x : α // x ∈ s }) : count a s.attach = count (↑a) s

theorem Multiset.count_pos {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} : 0 < count a s ↔ a ∈ s

theorem Multiset.one_le_count_iff_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} : 1 ≤ count a s ↔ a ∈ s

@[simp]

theorem Multiset.count_eq_zero_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} (h : a ∉ s) : count a s = 0

theorem Multiset.count_ne_zero {α : Type u_1} [DecidableEq α] {s : Multiset α} {a : α} : count a s ≠ 0 ↔ a ∈ s

@[simp]

theorem Multiset.count_eq_zero {α : Type u_1} [DecidableEq α] {s : Multiset α} {a : α} : count a s = 0 ↔ a ∉ s

theorem Multiset.count_eq_card {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} : count a s = s.card ↔ ∀ x ∈ s, a = x

@[simp]

theorem Multiset.count_replicate_self {α : Type u_1} [DecidableEq α] (a : α) (n : ℕ) : count a (replicate n a) = n

theorem Multiset.count_replicate {α : Type u_1} [DecidableEq α] (a b : α) (n : ℕ) : count a (replicate n b) = if b = a then n else 0

@[simp]

theorem Multiset.count_erase_self {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) : count a (s.erase a) = count a s - 1

@[simp]

theorem Multiset.count_erase_of_ne {α : Type u_1} [DecidableEq α] {a b : α} (ab : a ≠ b) (s : Multiset α) : count a (s.erase b) = count a s

theorem Multiset.le_count_iff_replicate_le {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} {n : ℕ} : n ≤ count a s ↔ replicate n a ≤ s

@[simp]

theorem Multiset.count_filter_of_pos {α : Type u_1} [DecidableEq α] {p : α → Prop} [DecidablePred p] {a : α} {s : Multiset α} (h : p a) : count a (filter p s) = count a s

@[simp]

theorem Multiset.count_filter_of_neg {α : Type u_1} [DecidableEq α] {p : α → Prop} [DecidablePred p] {a : α} {s : Multiset α} (h : ¬p a) : count a (filter p s) = 0

theorem Multiset.count_filter {α : Type u_1} [DecidableEq α] {p : α → Prop} [DecidablePred p] {a : α} {s : Multiset α} : count a (filter p s) = if p a then count a s else 0

theorem Multiset.ext {α : Type u_1} [DecidableEq α] {s t : Multiset α} : s = t ↔ ∀ (a : α), count a s = count a t

theorem Multiset.ext' {α : Type u_1} [DecidableEq α] {s t : Multiset α} : (∀ (a : α), count a s = count a t) → s = t

theorem Multiset.count_injective {α : Type u_1} [DecidableEq α] : Function.Injective fun (s : Multiset α) (a : α) => count a s

theorem Multiset.le_iff_count {α : Type u_1} [DecidableEq α] {s t : Multiset α} : s ≤ t ↔ ∀ (a : α), count a s ≤ count a t

theorem Multiset.count_map {α : Type u_3} {β : Type u_4} (f : α → β) (s : Multiset α) [DecidableEq β] (b : β) : count b (map f s) = (filter (fun (a : α) => b = f a) s).card

theorem Multiset.count_map_eq_count {α : Type u_1} {β : Type v} [DecidableEq α] [DecidableEq β] (f : α → β) (s : Multiset α) (hf : Set.InjOn f {x : α | x ∈ s}) (x : α) (H : x ∈ s) : count (f x) (map f s) = count x s

Multiset.map f preserves count if f is injective on the set of elements contained in the multiset

theorem Multiset.count_map_eq_count' {α : Type u_1} {β : Type v} [DecidableEq α] [DecidableEq β] (f : α → β) (s : Multiset α) (hf : Function.Injective f) (x : α) : count (f x) (map f s) = count x s

Multiset.map f preserves count if f is injective

theorem Multiset.filter_eq' {α : Type u_1} [DecidableEq α] (s : Multiset α) (b : α) : filter (fun (x : α) => x = b) s = replicate (count b s) b

theorem Multiset.filter_eq {α : Type u_1} [DecidableEq α] (s : Multiset α) (b : α) : filter (Eq b) s = replicate (count b s) b

theorem Multiset.erase_attach_map_val {α : Type u_1} [DecidableEq α] (s : Multiset α) (x : { x : α // x ∈ s }) : map Subtype.val (s.attach.erase x) = s.erase ↑x

theorem Multiset.erase_attach_map {α : Type u_1} {β : Type v} [DecidableEq α] (s : Multiset α) (f : α → β) (x : { x : α // x ∈ s }) : map (fun (j : { x : α // x ∈ s }) => f ↑j) (s.attach.erase x) = map f (s.erase ↑x)

theorem Multiset.add_left_inj {α : Type u_1} {s t u : Multiset α} : s + u = t + u ↔ s = t

theorem Multiset.add_right_inj {α : Type u_1} {s t u : Multiset α} : s + t = s + u ↔ t = u

Subtraction

def Multiset.sub {α : Type u_1} [DecidableEq α] (s t : Multiset α) : Multiset α

s - t is the multiset such that count a (s - t) = count a s - count a t for all a. (note that it is truncated subtraction, so count a (s - t) = 0 if count a s ≤ count a t).

Equations

• s.sub t = Quotient.liftOn₂ s t (fun (l₁ l₂ : List α) => ↑(l₁.diff l₂)) ⋯

instance Multiset.instSub {α : Type u_1} [DecidableEq α] : Sub (Multiset α)

Equations

• Multiset.instSub = { sub := Multiset.sub }

@[simp]

theorem Multiset.coe_sub {α : Type u_1} [DecidableEq α] (s t : List α) : ↑s - ↑t = ↑(s.diff t)

@[simp]

theorem Multiset.sub_zero {α : Type u_1} [DecidableEq α] (s : Multiset α) : s - 0 = s

This is a special case of tsub_zero, which should be used instead of this. This is needed to prove OrderedSub (Multiset α).

@[simp]

theorem Multiset.sub_cons {α : Type u_1} [DecidableEq α] (a : α) (s t : Multiset α) : s - a ::ₘ t = s.erase a - t

theorem Multiset.zero_sub {α : Type u_1} [DecidableEq α] (t : Multiset α) : 0 - t = 0

@[simp]

theorem Multiset.countP_sub {α : Type u_1} [DecidableEq α] {s t : Multiset α} : t ≤ s → ∀ (p : α → Prop) [inst : DecidablePred p], countP p (s - t) = countP p s - countP p t

@[simp]

theorem Multiset.count_sub {α : Type u_1} [DecidableEq α] (a : α) (s t : Multiset α) : count a (s - t) = count a s - count a t

theorem Multiset.sub_le_iff_le_add {α : Type u_1} [DecidableEq α] {s t u : Multiset α} : s - t ≤ u ↔ s ≤ u + t

This is a special case of tsub_le_iff_right, which should be used instead of this. This is needed to prove OrderedSub (Multiset α).

theorem Multiset.sub_le_iff_le_add' {α : Type u_1} [DecidableEq α] {s t u : Multiset α} : s - t ≤ u ↔ s ≤ t + u

This is a special case of tsub_le_iff_left, which should be used instead of this.

theorem Multiset.sub_le_self {α : Type u_1} [DecidableEq α] (s t : Multiset α) : s - t ≤ s

theorem Multiset.add_sub_assoc {α : Type u_1} [DecidableEq α] {s t u : Multiset α} (hut : u ≤ t) : s + t - u = s + (t - u)

theorem Multiset.add_sub_cancel {α : Type u_1} [DecidableEq α] {s t : Multiset α} (hts : t ≤ s) : s - t + t = s

theorem Multiset.sub_add_cancel {α : Type u_1} [DecidableEq α] {s t : Multiset α} (hts : t ≤ s) : s - t + t = s

theorem Multiset.sub_add_eq_sub_sub {α : Type u_1} [DecidableEq α] {s t u : Multiset α} : s - (t + u) = s - t - u

theorem Multiset.le_sub_add {α : Type u_1} [DecidableEq α] {s t : Multiset α} : s ≤ s - t + t

theorem Multiset.le_add_sub {α : Type u_1} [DecidableEq α] {s t : Multiset α} : s ≤ t + (s - t)

theorem Multiset.sub_le_sub_right {α : Type u_1} [DecidableEq α] {s t u : Multiset α} (hst : s ≤ t) : s - u ≤ t - u

theorem Multiset.add_sub_cancel_right {α : Type u_1} [DecidableEq α] {s t : Multiset α} : s + t - t = s

theorem Multiset.eq_sub_of_add_eq {α : Type u_1} [DecidableEq α] {s t u : Multiset α} (hstu : s + t = u) : s = u - t

@[simp]

theorem Multiset.filter_sub {α : Type u_1} [DecidableEq α] (p : α → Prop) [DecidablePred p] (s t : Multiset α) : filter p (s - t) = filter p s - filter p t

@[simp]

theorem Multiset.sub_filter_eq_filter_not {α : Type u_1} [DecidableEq α] (p : α → Prop) [DecidablePred p] (s : Multiset α) : s - filter p s = filter (fun (a : α) => ¬p a) s

theorem Multiset.cons_sub_of_le {α : Type u_1} [DecidableEq α] (a : α) {s t : Multiset α} (h : t ≤ s) : a ::ₘ s - t = a ::ₘ (s - t)

theorem Multiset.sub_eq_fold_erase {α : Type u_1} [DecidableEq α] (s t : Multiset α) : s - t = foldl erase s t

@[simp]

theorem Multiset.card_sub {α : Type u_1} [DecidableEq α] {s t : Multiset α} (h : t ≤ s) : (s - t).card = s.card - t.card

Union

def Multiset.union {α : Type u_1} [DecidableEq α] (s t : Multiset α) : Multiset α

s ∪ t is the multiset such that the multiplicity of each a in it is the maximum of the multiplicity of a in s and t. This is the supremum of multisets.

Equations

• s.union t = s - t + t

instance Multiset.instUnion {α : Type u_1} [DecidableEq α] : Union (Multiset α)

Equations

• Multiset.instUnion = { union := Multiset.union }

theorem Multiset.union_def {α : Type u_1} [DecidableEq α] (s t : Multiset α) : s ∪ t = s - t + t

theorem Multiset.le_union_left {α : Type u_1} [DecidableEq α] {s t : Multiset α} : s ≤ s ∪ t

theorem Multiset.le_union_right {α : Type u_1} [DecidableEq α] {s t : Multiset α} : t ≤ s ∪ t

theorem Multiset.eq_union_left {α : Type u_1} [DecidableEq α] {s t : Multiset α} : t ≤ s → s ∪ t = s

theorem Multiset.union_le_union_right {α : Type u_1} [DecidableEq α] {s t : Multiset α} (h : s ≤ t) (u : Multiset α) : s ∪ u ≤ t ∪ u

theorem Multiset.union_le {α : Type u_1} [DecidableEq α] {s t u : Multiset α} (h₁ : s ≤ u) (h₂ : t ≤ u) : s ∪ t ≤ u

@[simp]

theorem Multiset.mem_union {α : Type u_1} [DecidableEq α] {s t : Multiset α} {a : α} : a ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t

@[simp]

theorem Multiset.map_union {α : Type u_1} {β : Type v} [DecidableEq α] [DecidableEq β] {f : α → β} (finj : Function.Injective f) {s t : Multiset α} : map f (s ∪ t) = map f s ∪ map f t

@[simp]

theorem Multiset.zero_union {α : Type u_1} [DecidableEq α] {s : Multiset α} : 0 ∪ s = s

@[simp]

theorem Multiset.union_zero {α : Type u_1} [DecidableEq α] {s : Multiset α} : s ∪ 0 = s

@[simp]

theorem Multiset.count_union {α : Type u_1} [DecidableEq α] (a : α) (s t : Multiset α) : count a (s ∪ t) = count a s ⊔ count a t

@[simp]

theorem Multiset.filter_union {α : Type u_1} [DecidableEq α] (p : α → Prop) [DecidablePred p] (s t : Multiset α) : filter p (s ∪ t) = filter p s ∪ filter p t

Intersection

def Multiset.inter {α : Type u_1} [DecidableEq α] (s t : Multiset α) : Multiset α

s ∩ t is the multiset such that the multiplicity of each a in it is the minimum of the multiplicity of a in s and t. This is the infimum of multisets.

Equations

• s.inter t = Quotient.liftOn₂ s t (fun (l₁ l₂ : List α) => ↑(l₁.bagInter l₂)) ⋯

instance Multiset.instInter {α : Type u_1} [DecidableEq α] : Inter (Multiset α)

Equations

• Multiset.instInter = { inter := Multiset.inter }

@[simp]

theorem Multiset.inter_zero {α : Type u_1} [DecidableEq α] (s : Multiset α) : s ∩ 0 = 0

@[simp]

theorem Multiset.zero_inter {α : Type u_1} [DecidableEq α] (s : Multiset α) : 0 ∩ s = 0

@[simp]

theorem Multiset.cons_inter_of_pos {α : Type u_1} [DecidableEq α] {t : Multiset α} {a : α} (s : Multiset α) : a ∈ t → (a ::ₘ s) ∩ t = a ::ₘ s ∩ t.erase a

@[simp]

theorem Multiset.cons_inter_of_neg {α : Type u_1} [DecidableEq α] {t : Multiset α} {a : α} (s : Multiset α) : a ∉ t → (a ::ₘ s) ∩ t = s ∩ t

theorem Multiset.inter_le_left {α : Type u_1} [DecidableEq α] {s t : Multiset α} : s ∩ t ≤ s

theorem Multiset.inter_le_right {α : Type u_1} [DecidableEq α] {s t : Multiset α} : s ∩ t ≤ t

theorem Multiset.le_inter {α : Type u_1} [DecidableEq α] {s t u : Multiset α} (h₁ : s ≤ t) (h₂ : s ≤ u) : s ≤ t ∩ u

@[simp]

theorem Multiset.mem_inter {α : Type u_1} [DecidableEq α] {s t : Multiset α} {a : α} : a ∈ s ∩ t ↔ a ∈ s ∧ a ∈ t

instance Multiset.instLattice {α : Type u_1} [DecidableEq α] : Lattice (Multiset α)

Equations

• Multiset.instLattice = Lattice.mk (fun (x1 x2 : Multiset α) => x1 ∩ x2) ⋯ ⋯ ⋯

@[simp]

theorem Multiset.sup_eq_union {α : Type u_1} [DecidableEq α] (s t : Multiset α) : s ⊔ t = s ∪ t

@[simp]

theorem Multiset.inf_eq_inter {α : Type u_1} [DecidableEq α] (s t : Multiset α) : s ⊓ t = s ∩ t

@[simp]

theorem Multiset.le_inter_iff {α : Type u_1} [DecidableEq α] {s t u : Multiset α} : s ≤ t ∩ u ↔ s ≤ t ∧ s ≤ u

@[simp]

theorem Multiset.union_le_iff {α : Type u_1} [DecidableEq α] {s t u : Multiset α} : s ∪ t ≤ u ↔ s ≤ u ∧ t ≤ u

theorem Multiset.union_comm {α : Type u_1} [DecidableEq α] (s t : Multiset α) : s ∪ t = t ∪ s

theorem Multiset.inter_comm {α : Type u_1} [DecidableEq α] (s t : Multiset α) : s ∩ t = t ∩ s

theorem Multiset.eq_union_right {α : Type u_1} [DecidableEq α] {s t : Multiset α} (h : s ≤ t) : s ∪ t = t

theorem Multiset.union_le_union_left {α : Type u_1} [DecidableEq α] {s t : Multiset α} (h : s ≤ t) (u : Multiset α) : u ∪ s ≤ u ∪ t

theorem Multiset.union_le_add {α : Type u_1} [DecidableEq α] (s t : Multiset α) : s ∪ t ≤ s + t

theorem Multiset.union_add_distrib {α : Type u_1} [DecidableEq α] (s t u : Multiset α) : s ∪ t + u = s + u ∪ (t + u)

theorem Multiset.add_union_distrib {α : Type u_1} [DecidableEq α] (s t u : Multiset α) : s + (t ∪ u) = s + t ∪ (s + u)

theorem Multiset.cons_union_distrib {α : Type u_1} [DecidableEq α] (a : α) (s t : Multiset α) : a ::ₘ (s ∪ t) = a ::ₘ s ∪ a ::ₘ t

theorem Multiset.inter_add_distrib {α : Type u_1} [DecidableEq α] (s t u : Multiset α) : s ∩ t + u = (s + u) ∩ (t + u)

theorem Multiset.add_inter_distrib {α : Type u_1} [DecidableEq α] (s t u : Multiset α) : s + t ∩ u = (s + t) ∩ (s + u)

theorem Multiset.cons_inter_distrib {α : Type u_1} [DecidableEq α] (a : α) (s t : Multiset α) : a ::ₘ s ∩ t = (a ::ₘ s) ∩ (a ::ₘ t)

theorem Multiset.union_add_inter {α : Type u_1} [DecidableEq α] (s t : Multiset α) : s ∪ t + s ∩ t = s + t

theorem Multiset.sub_add_inter {α : Type u_1} [DecidableEq α] (s t : Multiset α) : s - t + s ∩ t = s

theorem Multiset.sub_inter {α : Type u_1} [DecidableEq α] (s t : Multiset α) : s - s ∩ t = s - t

@[simp]

theorem Multiset.count_inter {α : Type u_1} [DecidableEq α] (a : α) (s t : Multiset α) : count a (s ∩ t) = count a s ⊓ count a t

@[simp]

theorem Multiset.coe_inter {α : Type u_1} [DecidableEq α] (s t : List α) : ↑s ∩ ↑t = ↑(s.bagInter t)

instance Multiset.instDistribLattice {α : Type u_1} [DecidableEq α] : DistribLattice (Multiset α)

Equations

• Multiset.instDistribLattice = DistribLattice.mk ⋯

@[simp]

theorem Multiset.filter_inter {α : Type u_1} [DecidableEq α] (p : α → Prop) [DecidablePred p] (s t : Multiset α) : filter p (s ∩ t) = filter p s ∩ filter p t

@[simp]

theorem Multiset.replicate_inter {α : Type u_1} [DecidableEq α] (n : ℕ) (x : α) (s : Multiset α) : replicate n x ∩ s = replicate (n ⊓ count x s) x

@[simp]

theorem Multiset.inter_replicate {α : Type u_1} [DecidableEq α] (s : Multiset α) (n : ℕ) (x : α) : s ∩ replicate n x = replicate (count x s ⊓ n) x

@[simp]

theorem Multiset.map_le_map_iff {α : Type u_1} {β : Type v} {f : α → β} (hf : Function.Injective f) {s t : Multiset α} : map f s ≤ map f t ↔ s ≤ t

def Multiset.mapEmbedding {α : Type u_1} {β : Type v} (f : α ↪ β) : Multiset α ↪o Multiset β

Associate to an embedding f from α to β the order embedding that maps a multiset to its image under f.

Equations

• Multiset.mapEmbedding f = OrderEmbedding.ofMapLEIff (Multiset.map ⇑f) ⋯

@[simp]

theorem Multiset.mapEmbedding_apply {α : Type u_1} {β : Type v} (f : α ↪ β) (s : Multiset α) : (mapEmbedding f) s = map (⇑f) s

theorem Multiset.count_eq_card_filter_eq {α : Type u_1} [DecidableEq α] (s : Multiset α) (a : α) : count a s = (filter (fun (x : α) => a = x) s).card

@[simp]

theorem Multiset.map_count_True_eq_filter_card {α : Type u_1} (s : Multiset α) (p : α → Prop) [DecidablePred p] : count True (map p s) = (filter p s).card

Mapping a multiset through a predicate and counting the Trues yields the cardinality of the set filtered by the predicate. Note that this uses the notion of a multiset of Props - due to the decidability requirements of count, the decidability instance on the LHS is different from the RHS. In particular, the decidability instance on the left leaks Classical.decEq. See here for more discussion.

@[simp]

theorem Multiset.sub_singleton {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) : s - {a} = s.erase a

theorem Multiset.mem_sub {α : Type u_1} [DecidableEq α] {a : α} {s t : Multiset α} : a ∈ s - t ↔ count a t < count a s

theorem Multiset.inter_add_sub_of_add_eq_add {α : Type u_1} [DecidableEq α] {M N P Q : Multiset α} (h : M + N = P + Q) : N ∩ Q + (P - M) = N

Lift a relation to Multisets

inductive Multiset.Rel {α : Type u_1} {β : Type v} (r : α → β → Prop) : Multiset α → Multiset β → Prop

Rel r s t -- lift the relation r between two elements to a relation between s and t, s.t. there is a one-to-one mapping between elements in s and t following r.

• zero {α : Type u_1} {β : Type v} {r : α → β → Prop} : Rel r 0 0
• cons {α : Type u_1} {β : Type v} {r : α → β → Prop} {a : α} {b : β} {as : Multiset α} {bs : Multiset β} : r a b → Rel r as bs → Rel r (a ::ₘ as) (b ::ₘ bs)

theorem Multiset.rel_iff {α : Type u_1} {β : Type v} (r : α → β → Prop) (a✝ : Multiset α) (a✝¹ : Multiset β) : Rel r a✝ a✝¹ ↔ a✝ = 0 ∧ a✝¹ = 0 ∨ ∃ (a : α) (b : β) (as : Multiset α) (bs : Multiset β), r a b ∧ Rel r as bs ∧ a✝ = a ::ₘ as ∧ a✝¹ = b ::ₘ bs

theorem Multiset.rel_flip {α : Type u_1} {β : Type v} {r : α → β → Prop} {s : Multiset β} {t : Multiset α} : Rel (flip r) s t ↔ Rel r t s

theorem Multiset.rel_refl_of_refl_on {α : Type u_1} {m : Multiset α} {r : α → α → Prop} : (∀ x ∈ m, r x x) → Rel r m m

theorem Multiset.rel_eq_refl {α : Type u_1} {s : Multiset α} : Rel (fun (x1 x2 : α) => x1 = x2) s s

theorem Multiset.rel_eq {α : Type u_1} {s t : Multiset α} : Rel (fun (x1 x2 : α) => x1 = x2) s t ↔ s = t

theorem Multiset.Rel.mono {α : Type u_1} {β : Type v} {r p : α → β → Prop} {s : Multiset α} {t : Multiset β} (hst : Rel r s t) (h : ∀ a ∈ s, ∀ b ∈ t, r a b → p a b) : Rel p s t

theorem Multiset.Rel.add {α : Type u_1} {β : Type v} {r : α → β → Prop} {s : Multiset α} {t : Multiset β} {u : Multiset α} {v : Multiset β} (hst : Rel r s t) (huv : Rel r u v) : Rel r (s + u) (t + v)

theorem Multiset.rel_flip_eq {α : Type u_1} {s t : Multiset α} : Rel (fun (a b : α) => b = a) s t ↔ s = t

@[simp]

theorem Multiset.rel_zero_left {α : Type u_1} {β : Type v} {r : α → β → Prop} {b : Multiset β} : Rel r 0 b ↔ b = 0

@[simp]

theorem Multiset.rel_zero_right {α : Type u_1} {β : Type v} {r : α → β → Prop} {a : Multiset α} : Rel r a 0 ↔ a = 0

theorem Multiset.rel_cons_left {α : Type u_1} {β : Type v} {r : α → β → Prop} {a : α} {as : Multiset α} {bs : Multiset β} : Rel r (a ::ₘ as) bs ↔ ∃ (b : β) (bs' : Multiset β), r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'

theorem Multiset.rel_cons_right {α : Type u_1} {β : Type v} {r : α → β → Prop} {as : Multiset α} {b : β} {bs : Multiset β} : Rel r as (b ::ₘ bs) ↔ ∃ (a : α) (as' : Multiset α), r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'

theorem Multiset.rel_add_left {α : Type u_1} {β : Type v} {r : α → β → Prop} {as₀ as₁ : Multiset α} {bs : Multiset β} : Rel r (as₀ + as₁) bs ↔ ∃ (bs₀ : Multiset β) (bs₁ : Multiset β), Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁

theorem Multiset.rel_add_right {α : Type u_1} {β : Type v} {r : α → β → Prop} {as : Multiset α} {bs₀ bs₁ : Multiset β} : Rel r as (bs₀ + bs₁) ↔ ∃ (as₀ : Multiset α) (as₁ : Multiset α), Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁

theorem Multiset.rel_map_left {α : Type u_1} {β : Type v} {γ : Type u_2} {r : α → β → Prop} {s : Multiset γ} {f : γ → α} {t : Multiset β} : Rel r (map f s) t ↔ Rel (fun (a : γ) (b : β) => r (f a) b) s t

theorem Multiset.rel_map_right {α : Type u_1} {β : Type v} {γ : Type u_2} {r : α → β → Prop} {s : Multiset α} {t : Multiset γ} {f : γ → β} : Rel r s (map f t) ↔ Rel (fun (a : α) (b : γ) => r a (f b)) s t

theorem Multiset.rel_map {α : Type u_1} {β : Type v} {γ : Type u_2} {δ : Type u_3} {p : γ → δ → Prop} {s : Multiset α} {t : Multiset β} {f : α → γ} {g : β → δ} : Rel p (map f s) (map g t) ↔ Rel (fun (a : α) (b : β) => p (f a) (g b)) s t

theorem Multiset.card_eq_card_of_rel {α : Type u_1} {β : Type v} {r : α → β → Prop} {s : Multiset α} {t : Multiset β} (h : Rel r s t) : s.card = t.card

theorem Multiset.exists_mem_of_rel_of_mem {α : Type u_1} {β : Type v} {r : α → β → Prop} {s : Multiset α} {t : Multiset β} (h : Rel r s t) {a : α} : a ∈ s → ∃ b ∈ t, r a b

theorem Multiset.rel_of_forall {α : Type u_1} {m1 m2 : Multiset α} {r : α → α → Prop} (h : ∀ (a b : α), a ∈ m1 → b ∈ m2 → r a b) (hc : m1.card = m2.card) : Rel r m1 m2

theorem Multiset.rel_replicate_left {α : Type u_1} {m : Multiset α} {a : α} {r : α → α → Prop} {n : ℕ} : Rel r (replicate n a) m ↔ m.card = n ∧ ∀ x ∈ m, r a x

theorem Multiset.rel_replicate_right {α : Type u_1} {m : Multiset α} {a : α} {r : α → α → Prop} {n : ℕ} : Rel r m (replicate n a) ↔ m.card = n ∧ ∀ x ∈ m, r x a

theorem Multiset.Rel.trans {α : Type u_1} (r : α → α → Prop) [IsTrans α r] {s t u : Multiset α} (r1 : Rel r s t) (r2 : Rel r t u) : Rel r s u

theorem Multiset.Rel.countP_eq {α : Type u_1} (r : α → α → Prop) [IsTrans α r] [IsSymm α r] {s t : Multiset α} (x : α) [DecidablePred (r x)] (h : Rel r s t) : countP (r x) s = countP (r x) t

theorem Multiset.map_eq_map {α : Type u_1} {β : Type v} {f : α → β} (hf : Function.Injective f) {s t : Multiset α} : map f s = map f t ↔ s = t

theorem Multiset.map_injective {α : Type u_1} {β : Type v} {f : α → β} (hf : Function.Injective f) : Function.Injective (map f)

theorem Multiset.filter_attach' {α : Type u_1} (s : Multiset α) (p : { a : α // a ∈ s } → Prop) [DecidableEq α] [DecidablePred p] : filter p s.attach = map (Subtype.map id ⋯) (filter (fun (x : α) => ∃ (h : x ∈ s), p ⟨x, h⟩) s).attach

theorem Multiset.map_mk_eq_map_mk_of_rel {α : Type u_1} {r : α → α → Prop} {s t : Multiset α} (hst : Rel r s t) : map (Quot.mk r) s = map (Quot.mk r) t

theorem Multiset.exists_multiset_eq_map_quot_mk {α : Type u_1} {r : α → α → Prop} (s : Multiset (Quot r)) : ∃ (t : Multiset α), s = map (Quot.mk r) t

theorem Multiset.induction_on_multiset_quot {α : Type u_1} {r : α → α → Prop} {p : Multiset (Quot r) → Prop} (s : Multiset (Quot r)) : (∀ (s : Multiset α), p (map (Quot.mk r) s)) → p s

Disjoint multisets

@[deprecated Disjoint (since := "2024-11-01")]

def Multiset.Disjoint {α : Type u_1} (s t : Multiset α) : Prop

Disjoint s t means that s and t have no elements in common.

Equations

• s.Disjoint t = ∀ ⦃a : α⦄, a ∈ s → a ∈ t → False

theorem Multiset.disjoint_left {α : Type u_1} {s t : Multiset α} : Disjoint s t ↔ ∀ {a : α}, a ∈ s → a ∉ t

@[simp]

theorem Multiset.coe_disjoint {α : Type u_1} (l₁ l₂ : List α) : Disjoint ↑l₁ ↑l₂ ↔ l₁.Disjoint l₂

@[deprecated Disjoint.symm (since := "2024-11-01")]

theorem Multiset.Disjoint.symm {α : Type u_1} [PartialOrder α] [OrderBot α] ⦃a b : α⦄ : Disjoint a b → Disjoint b a

Alias of Disjoint.symm.

@[deprecated disjoint_comm (since := "2024-11-01")]

theorem Multiset.disjoint_comm {α : Type u_1} [PartialOrder α] [OrderBot α] {a b : α} : Disjoint a b ↔ Disjoint b a

Alias of disjoint_comm.

theorem Multiset.disjoint_right {α : Type u_1} {s t : Multiset α} : Disjoint s t ↔ ∀ {a : α}, a ∈ t → a ∉ s

theorem Multiset.disjoint_iff_ne {α : Type u_1} {s t : Multiset α} : Disjoint s t ↔ ∀ a ∈ s, ∀ b ∈ t, a ≠ b

theorem Multiset.disjoint_of_subset_left {α : Type u_1} {s t u : Multiset α} (h : s ⊆ u) (d : Disjoint u t) : Disjoint s t

theorem Multiset.disjoint_of_subset_right {α : Type u_1} {s t u : Multiset α} (h : t ⊆ u) (d : Disjoint s u) : Disjoint s t

@[deprecated Disjoint.mono_left (since := "2024-11-01")]

theorem Multiset.disjoint_of_le_left {α : Type u_1} [PartialOrder α] [OrderBot α] {a b c : α} (h : a ≤ b) : Disjoint b c → Disjoint a c

Alias of Disjoint.mono_left.

@[deprecated Disjoint.mono_right (since := "2024-11-01")]

theorem Multiset.disjoint_of_le_right {α : Type u_1} [PartialOrder α] [OrderBot α] {a b c : α} : b ≤ c → Disjoint a c → Disjoint a b

Alias of Disjoint.mono_right.

@[simp]

theorem Multiset.zero_disjoint {α : Type u_1} (l : Multiset α) : Disjoint 0 l

@[simp]

theorem Multiset.singleton_disjoint {α : Type u_1} {l : Multiset α} {a : α} : Disjoint {a} l ↔ a ∉ l

@[simp]

theorem Multiset.disjoint_singleton {α : Type u_1} {l : Multiset α} {a : α} : Disjoint l {a} ↔ a ∉ l

@[simp]

theorem Multiset.disjoint_add_left {α : Type u_1} {s t u : Multiset α} : Disjoint (s + t) u ↔ Disjoint s u ∧ Disjoint t u

@[simp]

theorem Multiset.disjoint_add_right {α : Type u_1} {s t u : Multiset α} : Disjoint s (t + u) ↔ Disjoint s t ∧ Disjoint s u

@[simp]

theorem Multiset.disjoint_cons_left {α : Type u_1} {a : α} {s t : Multiset α} : Disjoint (a ::ₘ s) t ↔ a ∉ t ∧ Disjoint s t

@[simp]

theorem Multiset.disjoint_cons_right {α : Type u_1} {a : α} {s t : Multiset α} : Disjoint s (a ::ₘ t) ↔ a ∉ s ∧ Disjoint s t

theorem Multiset.inter_eq_zero_iff_disjoint {α : Type u_1} [DecidableEq α] {s t : Multiset α} : s ∩ t = 0 ↔ Disjoint s t

@[simp]

theorem Multiset.disjoint_union_left {α : Type u_1} [DecidableEq α] {s t u : Multiset α} : Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u

@[simp]

theorem Multiset.disjoint_union_right {α : Type u_1} [DecidableEq α] {s t u : Multiset α} : Disjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u

theorem Multiset.add_eq_union_iff_disjoint {α : Type u_1} [DecidableEq α] {s t : Multiset α} : s + t = s ∪ t ↔ Disjoint s t

theorem Multiset.add_eq_union_left_of_le {α : Type u_1} [DecidableEq α] {s t u : Multiset α} (h : t ≤ s) : u + s = u ∪ t ↔ Disjoint u s ∧ s = t

theorem Multiset.add_eq_union_right_of_le {α : Type u_1} [DecidableEq α] {x y z : Multiset α} (h : z ≤ y) : x + y = x ∪ z ↔ y = z ∧ Disjoint x y

theorem Multiset.disjoint_map_map {α : Type u_1} {β : Type v} {γ : Type u_2} {f : α → γ} {g : β → γ} {s : Multiset α} {t : Multiset β} : Disjoint (map f s) (map g t) ↔ ∀ a ∈ s, ∀ b ∈ t, f a ≠ g b

def Multiset.Pairwise {α : Type u_1} (r : α → α → Prop) (m : Multiset α) : Prop

Pairwise r m states that there exists a list of the elements s.t. r holds pairwise on this list.

Equations

• Multiset.Pairwise r m = ∃ (l : List α), m = ↑l ∧ List.Pairwise r l

@[simp]

theorem Multiset.pairwise_zero {α : Type u_1} (r : α → α → Prop) : Pairwise r 0

theorem Multiset.pairwise_coe_iff {α : Type u_1} {r : α → α → Prop} {l : List α} : Pairwise r ↑l ↔ ∃ (l' : List α), l.Perm l' ∧ List.Pairwise r l'

theorem Multiset.pairwise_coe_iff_pairwise {α : Type u_1} {r : α → α → Prop} (hr : Symmetric r) {l : List α} : Pairwise r ↑l ↔ List.Pairwise r l

theorem Multiset.map_set_pairwise {α : Type u_1} {β : Type v} {f : α → β} {r : β → β → Prop} {m : Multiset α} (h : {a : α | a ∈ m}.Pairwise fun (a₁ a₂ : α) => r (f a₁) (f a₂)) : {b : β | b ∈ map f m}.Pairwise r

def Multiset.chooseX {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : Multiset α) (_hp : ∃! a : α, a ∈ l ∧ p a) : { a : α // a ∈ l ∧ p a }

Given a proof hp that there exists a unique a ∈ l such that p a, chooseX p l hp returns that a together with proofs of a ∈ l and p a.

Equations

• One or more equations did not get rendered due to their size.

def Multiset.choose {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : Multiset α) (hp : ∃! a : α, a ∈ l ∧ p a) : α

Given a proof hp that there exists a unique a ∈ l such that p a, choose p l hp returns that a.

Equations

• Multiset.choose p l hp = ↑(Multiset.chooseX p l hp)

theorem Multiset.choose_spec {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : Multiset α) (hp : ∃! a : α, a ∈ l ∧ p a) : choose p l hp ∈ l ∧ p (choose p l hp)

theorem Multiset.choose_mem {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : Multiset α) (hp : ∃! a : α, a ∈ l ∧ p a) : choose p l hp ∈ l

theorem Multiset.choose_property {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : Multiset α) (hp : ∃! a : α, a ∈ l ∧ p a) : p (choose p l hp)

def Multiset.subsingletonEquiv (α : Type u_1) [Subsingleton α] : List α ≃ Multiset α

The equivalence between lists and multisets of a subsingleton type.

Equations

• Multiset.subsingletonEquiv α = { toFun := Multiset.ofList, invFun := Quot.lift id ⋯, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Multiset.coe_subsingletonEquiv {α : Type u_1} [Subsingleton α] : ⇑(subsingletonEquiv α) = ofList