Documentation

theorem Multiset.induction_on {α : Type u_1} {p : Multiset α → Prop} (s : Multiset α) (h₁ : p 0) (h₂ : ⦃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_2} (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

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

def Multiset.recOn {α : Type u_1} {C : Multiset α → Sort u_2} (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

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

@[simp]

theorem Multiset.recOn_0 {α : Type u_2} {C : Multiset α → Sort u_1} {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_2} {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 α) :

Multiset.recOn (a ::ₘ m) C_0 C_cons C_cons_heq = C_cons a m (Multiset.recOn m C_0 C_cons C_cons_heq)

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

Prop

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

Equations

Multiset.Mem a s = Quot.liftOn s (fun l => a ∈ l) (_ : ∀ (l₁ l₂ : List α), l₁ ~ l₂ → (fun l => a ∈ l) l₁ = (fun l => a ∈ l) l₂)

instance Multiset.instMembershipMultiset {α : Type u_1} :

Membership α (Multiset α)

Equations

Multiset.instMembershipMultiset = { mem := Multiset.Mem }

@[simp]

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

a ∈ ↑l ↔ a ∈ l

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

Decidable (a ∈ s)

Equations

Multiset.decidableMem a s = Quot.recOnSubsingleton' s fun l => 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 : α) → x ∈ a ::ₘ s → p x) ↔ p a ∧ ((x : α) → x ∈ s → p x)

theorem Multiset.exists_cons_of_mem {α : Type u_1} {s : Multiset α} {a : α} :

a ∈ s → ∃ t, 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 : Multiset α} {bs : Multiset α} :

a ::ₘ as = b ::ₘ bs ↔ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs

Singleton #

instance Multiset.instSingletonMultiset {α : Type u_1} :

Singleton α (Multiset α)

Equations

Multiset.instSingletonMultiset = { singleton := fun a => a ::ₘ 0 }

instance Multiset.instIsLawfulSingletonMultisetInstEmptyCollectionMultisetInstInsertMultisetInstSingletonMultiset {α : Type u_1} :

IsLawfulSingleton α (Multiset α)

Equations

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

@[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 : Multiset α) (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

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

instance Multiset.instHasSubsetMultiset {α : Type u_1} :

HasSubset (Multiset α)

Equations

Multiset.instHasSubsetMultiset = { Subset := Multiset.Subset }

instance Multiset.instHasSSubsetMultiset {α : Type u_1} :

HasSSubset (Multiset α)

Equations

Multiset.instHasSSubsetMultiset = { SSubset := fun s t => s ⊆ t ∧ ¬t ⊆ s }

@[simp]

theorem Multiset.coe_subset {α : Type u_1} {l₁ : List α} {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 : Multiset α} {t : Multiset α} {u : Multiset α} :

s ⊆ t → t ⊆ u → s ⊆ u

theorem Multiset.subset_iff {α : Type u_1} {s : Multiset α} {t : Multiset α} :

s ⊆ t ↔ ∀ ⦃x : α⦄, x ∈ s → x ∈ t

theorem Multiset.mem_of_subset {α : Type u_1} {s : Multiset α} {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 : Multiset α} {t : Multiset α} :

a ::ₘ s ⊆ t ↔ a ∈ t ∧ s ⊆ t

theorem Multiset.cons_subset_cons {α : Type u_1} {a : α} {s : Multiset α} {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

theorem Multiset.subset_zero {α : Type u_1} {s : Multiset α} :

s ⊆ 0 ↔ s = 0

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

Multiset.toList s = Quotient.out' s

@[simp]

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

↑(Multiset.toList s) = s

@[simp]

theorem Multiset.toList_eq_nil {α : Type u_1} {s : Multiset α} :

Multiset.toList s = [] ↔ s = 0

@[simp]

theorem Multiset.empty_toList {α : Type u_1} {s : Multiset α} :

List.isEmpty (Multiset.toList s) = true ↔ s = 0

@[simp]

theorem Multiset.toList_zero {α : Type u_1} :

Multiset.toList 0 = []

@[simp]

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

a ∈ Multiset.toList s ↔ a ∈ s

@[simp]

theorem Multiset.toList_eq_singleton_iff {α : Type u_1} {a : α} {m : Multiset α} :

Multiset.toList m = [a] ↔ m = {a}

@[simp]

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

Multiset.toList {a} = [a]

Partial order on `Multiset`s #

def Multiset.Le {α : Type u_1} (s : Multiset α) (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

Multiset.Le s t = Quotient.liftOn₂ s t (fun x x_1 => x <+~ x_1) (_ : ∀ (x x_1 x_2 x_3 : List α), x ≈ x_2 → x_1 ≈ x_3 → (x <+~ x_1) = (x_2 <+~ x_3))

instance Multiset.instPartialOrderMultiset {α : Type u_1} :

PartialOrder (Multiset α)

Equations

Multiset.instPartialOrderMultiset = PartialOrder.mk (_ : ∀ (a b : Multiset α), a ≤ b → b ≤ a → a = b)

instance Multiset.decidableLE {α : Type u_1} [inst : DecidableEq α] :

DecidableRel fun x x_1 => x ≤ x_1

Equations

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

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

s ≤ t → s ⊆ t

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

s ≤ t → s ⊆ t

Alias of Multiset.subset_of_le.

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

a ∈ s → a ∈ t

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

¬a ∈ t → ¬a ∈ s

@[simp]

theorem Multiset.coe_le {α : Type u_1} {l₁ : List α} {l₂ : List α} :

↑l₁ ≤ ↑l₂ ↔ l₁ <+~ l₂

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

C s t

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

0 ≤ s

instance Multiset.instOrderBotMultisetToLEToPreorderInstPartialOrderMultiset {α : Type u_1} :

OrderBot (Multiset α)

Equations

Multiset.instOrderBotMultisetToLEToPreorderInstPartialOrderMultiset = OrderBot.mk (_ : ∀ (s : Multiset α), 0 ≤ s)

@[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 : Multiset α} {t : Multiset α} (a : α) :

a ::ₘ s ≤ a ::ₘ t ↔ s ≤ t

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

s ≤ t → a ::ₘ s ≤ a ::ₘ t

theorem Multiset.le_cons_of_not_mem {α : Type u_1} {s : Multiset α} {t : Multiset α} {a : α} (m : ¬a ∈ s) :

s ≤ a ::ₘ t ↔ s ≤ t

@[simp]

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

{a} ≠ 0

@[simp]

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

{a} ≤ s ↔ a ∈ s

Additive monoid #

def Multiset.add {α : Type u_1} (s₁ : Multiset α) (s₂ : 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

Multiset.add s₁ s₂ = Quotient.liftOn₂ s₁ s₂ (fun l₁ l₂ => ↑(l₁ ++ l₂)) (_ : ∀ (x x_1 x_2 x_3 : List α), x ≈ x_2 → x_1 ≈ x_3 → Quot.mk Setoid.r (x ++ x_1) = Quot.mk Setoid.r (x_2 ++ x_3))

instance Multiset.instAddMultiset {α : Type u_1} :

Add (Multiset α)

Equations

Multiset.instAddMultiset = { add := Multiset.add }

@[simp]

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

↑s + ↑t = ↑(s ++ t)

@[simp]

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

{a} + s = a ::ₘ s

instance Multiset.instCovariantClassMultisetHAddInstHAddInstAddMultisetLeToLEToPreorderInstPartialOrderMultiset {α : Type u_1} :

CovariantClass (Multiset α) (Multiset α) (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

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

instance Multiset.instContravariantClassMultisetHAddInstHAddInstAddMultisetLeToLEToPreorderInstPartialOrderMultiset {α : Type u_1} :

ContravariantClass (Multiset α) (Multiset α) (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

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

instance Multiset.instOrderedCancelAddCommMonoidMultiset {α : Type u_1} :

OrderedCancelAddCommMonoid (Multiset α)

Equations

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

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

s ≤ s + t

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

s ≤ t + s

theorem Multiset.le_iff_exists_add {α : Type u_1} {s : Multiset α} {t : Multiset α} :

s ≤ t ↔ ∃ u, t = s + u

instance Multiset.instCanonicallyOrderedAddMonoidMultiset {α : Type u_1} :

CanonicallyOrderedAddMonoid (Multiset α)

Equations

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

@[simp]

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

a ::ₘ s + t = a ::ₘ (s + t)

@[simp]

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

s + a ::ₘ t = a ::ₘ (s + t)

@[simp]

theorem Multiset.mem_add {α : Type u_1} {a : α} {s : Multiset α} {t : Multiset α} :

a ∈ s + t ↔ a ∈ s ∨ a ∈ t

theorem Multiset.mem_of_mem_nsmul {α : Type u_1} {a : α} {s : Multiset α} {n : ℕ} (h : a ∈ n • s) :

a ∈ s

@[simp]

theorem Multiset.mem_nsmul {α : Type u_1} {a : α} {s : Multiset α} {n : ℕ} (h0 : n ≠ 0) :

a ∈ n • s ↔ a ∈ s

theorem Multiset.nsmul_cons {α : Type u_1} {s : Multiset α} (n : ℕ) (a : α) :

n • (a ::ₘ s) = n • {a} + n • s

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

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

@[simp]

theorem Multiset.coe_card {α : Type u_1} (l : List α) :

↑Multiset.card ↑l = List.length l

@[simp]

theorem Multiset.length_toList {α : Type u_1} (s : Multiset α) :

List.length (Multiset.toList s) = ↑Multiset.card s

@[simp]

theorem Multiset.card_zero {α : Type u_1} :

↑Multiset.card 0 = 0

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

↑Multiset.card (s + t) = ↑Multiset.card s + ↑Multiset.card t

theorem Multiset.card_nsmul {α : Type u_1} (s : Multiset α) (n : ℕ) :

↑Multiset.card (n • s) = n * ↑Multiset.card s

@[simp]

theorem Multiset.card_cons {α : Type u_1} (a : α) (s : Multiset α) :

↑Multiset.card (a ::ₘ s) = ↑Multiset.card s + 1

@[simp]

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

↑Multiset.card {a} = 1

theorem Multiset.card_pair {α : Type u_1} (a : α) (b : α) :

↑Multiset.card {a, b} = 2

theorem Multiset.card_eq_one {α : Type u_1} {s : Multiset α} :

↑Multiset.card s = 1 ↔ ∃ a, s = {a}

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

↑Multiset.card s ≤ ↑Multiset.card t

theorem Multiset.card_mono {α : Type u_1} :

Monotone ↑Multiset.card

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

↑Multiset.card t ≤ ↑Multiset.card s → s = t

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

↑Multiset.card s < ↑Multiset.card t

theorem Multiset.lt_iff_cons_le {α : Type u_1} {s : Multiset α} {t : Multiset α} :

s < t ↔ ∃ a, a ::ₘ s ≤ t

@[simp]

theorem Multiset.card_eq_zero {α : Type u_1} {s : Multiset α} :

↑Multiset.card s = 0 ↔ s = 0

theorem Multiset.card_pos {α : Type u_1} {s : Multiset α} :

0 < ↑Multiset.card s ↔ s ≠ 0

theorem Multiset.card_pos_iff_exists_mem {α : Type u_1} {s : Multiset α} :

0 < ↑Multiset.card s ↔ ∃ a, a ∈ s

theorem Multiset.card_eq_two {α : Type u_1} {s : Multiset α} :

↑Multiset.card s = 2 ↔ ∃ x y, s = {x, y}

theorem Multiset.card_eq_three {α : Type u_1} {s : Multiset α} :

↑Multiset.card s = 3 ↔ ∃ x y z, s = {x, y, z}

Induction principles #

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

p s

The strong induction principle for multisets.

Equations

Multiset.strongInductionOn s ih = ih s fun t _h => Multiset.strongInductionOn t ih

theorem Multiset.strongInductionOn_eq {α : Type u_1} {p : Multiset α → Sort u_2} (s : Multiset α) (H : (s : Multiset α) → ((t : Multiset α) → t < s → p t) → p s) :

Multiset.strongInductionOn s H = H s fun t _h => Multiset.strongInductionOn t H

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

p s

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

↑Multiset.card s ≤ 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} ht _h => Multiset.strongDownwardInduction H t ht

theorem Multiset.strongDownwardInduction_eq {α : Type u_1} {p : Multiset α → Sort u_2} {n : ℕ} (H : (t₁ : Multiset α) → ({t₂ : Multiset α} → ↑Multiset.card t₂ ≤ n → t₁ < t₂ → p t₂) → ↑Multiset.card t₁ ≤ n → p t₁) (s : Multiset α) :

Multiset.strongDownwardInduction H s = H s fun {t₂} ht _hst => Multiset.strongDownwardInduction H t₂ ht

def Multiset.strongDownwardInductionOn {α : Type u_1} {p : Multiset α → Sort u_2} {n : ℕ} (s : Multiset α) :

((t₁ : Multiset α) → ({t₂ : Multiset α} → ↑Multiset.card t₂ ≤ n → t₁ < t₂ → p t₂) → ↑Multiset.card t₁ ≤ n → p t₁) → ↑Multiset.card s ≤ n → p s

Analogue of strongDownwardInduction with order of arguments swapped.

Equations

Multiset.strongDownwardInductionOn s H = Multiset.strongDownwardInduction H s

theorem Multiset.strongDownwardInductionOn_eq {α : Type u_1} {p : Multiset α → Sort u_2} (s : Multiset α) {n : ℕ} (H : (t₁ : Multiset α) → ({t₂ : Multiset α} → ↑Multiset.card t₂ ≤ n → t₁ < t₂ → p t₂) → ↑Multiset.card t₁ ≤ n → p t₁) :

(fun a => Multiset.strongDownwardInductionOn s H a) = H s fun {t} ht _h => Multiset.strongDownwardInductionOn t H ht

theorem Multiset.wellFounded_lt {α : Type u_1} :

WellFounded fun x x_1 => x < x_1

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

instance Multiset.is_wellFounded_lt {α : Type u_1} :

WellFoundedLT (Multiset α)

Equations

@Multiset.is_wellFounded_lt = @Multiset.is_wellFounded_lt.proof_1

`Multiset.replicate` #

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

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) = Multiset.replicate n a

@[simp]

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

Multiset.replicate 0 a = 0

@[simp]

theorem Multiset.replicate_succ {α : Type u_1} (a : α) (n : ℕ) :

Multiset.replicate (n + 1) a = a ::ₘ Multiset.replicate n a

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

Multiset.replicate (m + n) a = Multiset.replicate m a + Multiset.replicate n a

@[simp]

theorem Multiset.replicateAddMonoidHom_apply {α : Type u_1} (a : α) (n : ℕ) :

↑(Multiset.replicateAddMonoidHom a) n = Multiset.replicate n a

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

ℕ →+ Multiset α

Multiset.replicate as an AddMonoidHom.

Equations

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

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

Multiset.replicate 1 a = {a}

@[simp]

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

↑Multiset.card (Multiset.replicate n a) = n

theorem Multiset.mem_replicate {α : Type u_1} {a : α} {b : α} {n : ℕ} :

b ∈ Multiset.replicate n a ↔ n ≠ 0 ∧ b = a

theorem Multiset.eq_of_mem_replicate {α : Type u_1} {a : α} {b : α} {n : ℕ} :

b ∈ Multiset.replicate n a → b = a

theorem Multiset.eq_replicate_card {α : Type u_1} {a : α} {s : Multiset α} :

s = Multiset.replicate (↑Multiset.card s) a ↔ ∀ (b : α), b ∈ s → b = a

theorem Multiset.eq_replicate_of_mem {α : Type u_1} {a : α} {s : Multiset α} :

(∀ (b : α), b ∈ s → b = a) → s = Multiset.replicate (↑Multiset.card s) a

Alias of the reverse direction of Multiset.eq_replicate_card.

theorem Multiset.eq_replicate {α : Type u_1} {a : α} {n : ℕ} {s : Multiset α} :

s = Multiset.replicate n a ↔ ↑Multiset.card s = n ∧ ∀ (b : α), b ∈ s → b = a

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

Function.Injective (Multiset.replicate n)

@[simp]

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

Multiset.replicate n a = Multiset.replicate n b ↔ a = b

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

Function.Injective fun x => Multiset.replicate x a

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

Multiset.replicate n a ⊆ {a}

theorem Multiset.replicate_le_coe {α : Type u_1} {a : α} {n : ℕ} {l : List α} :

Multiset.replicate n a ≤ ↑l ↔ List.Sublist (List.replicate n a) l

theorem Multiset.nsmul_replicate {α : Type u_1} {a : α} (n : ℕ) (m : ℕ) :

n • Multiset.replicate m a = Multiset.replicate (n * m) a

theorem Multiset.nsmul_singleton {α : Type u_1} (a : α) (n : ℕ) :

n • {a} = Multiset.replicate n a

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

Multiset.replicate k a ≤ Multiset.replicate n a ↔ k ≤ n

theorem Multiset.le_replicate_iff {α : Type u_1} {m : Multiset α} {a : α} {n : ℕ} :

m ≤ Multiset.replicate n a ↔ ∃ k, k ≤ n ∧ m = Multiset.replicate k a

theorem Multiset.lt_replicate_succ {α : Type u_1} {m : Multiset α} {x : α} {n : ℕ} :

m < Multiset.replicate (n + 1) x ↔ m ≤ Multiset.replicate n x

Erasing one copy of an element #

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

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

Equations

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

@[simp]

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

Multiset.erase (↑l) a = ↑(List.erase l a)

@[simp]

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

Multiset.erase 0 a = 0

@[simp]

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

Multiset.erase (a ::ₘ s) a = s

@[simp]

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

Multiset.erase (b ::ₘ s) a = b ::ₘ Multiset.erase s a

@[simp]

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

Multiset.erase {a} a = 0

@[simp]

theorem Multiset.erase_of_not_mem {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α} :

¬a ∈ s → Multiset.erase s a = s

@[simp]

theorem Multiset.cons_erase {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {a : α} :

a ∈ s → a ::ₘ Multiset.erase s a = s

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

s ≤ a ::ₘ Multiset.erase s a

theorem Multiset.add_singleton_eq_iff {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {t : Multiset α} {a : α} :

s + {a} = t ↔ a ∈ t ∧ s = Multiset.erase t a

theorem Multiset.erase_add_left_pos {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α} (t : Multiset α) :

a ∈ s → Multiset.erase (s + t) a = Multiset.erase s a + t

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

Multiset.erase (s + t) a = s + Multiset.erase t a

theorem Multiset.erase_add_right_neg {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α} (t : Multiset α) :

¬a ∈ s → Multiset.erase (s + t) a = s + Multiset.erase t a

theorem Multiset.erase_add_left_neg {α : Type u_1} [inst : DecidableEq α] {a : α} (s : Multiset α) {t : Multiset α} (h : ¬a ∈ t) :

Multiset.erase (s + t) a = Multiset.erase s a + t

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

Multiset.erase s a ≤ s

@[simp]

theorem Multiset.erase_lt {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α} :

Multiset.erase s a < s ↔ a ∈ s

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

Multiset.erase s a ⊆ s

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

a ∈ Multiset.erase s b ↔ a ∈ s

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

a ∈ Multiset.erase s b → a ∈ s

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

Multiset.erase (Multiset.erase s a) b = Multiset.erase (Multiset.erase s b) a

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

Multiset.erase s a ≤ Multiset.erase t a

theorem Multiset.erase_le_iff_le_cons {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {t : Multiset α} {a : α} :

Multiset.erase s a ≤ t ↔ s ≤ a ::ₘ t

@[simp]

theorem Multiset.card_erase_of_mem {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α} :

a ∈ s → ↑Multiset.card (Multiset.erase s a) = Nat.pred (↑Multiset.card s)

@[simp]

theorem Multiset.card_erase_add_one {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α} :

a ∈ s → ↑Multiset.card (Multiset.erase s a) + 1 = ↑Multiset.card s

theorem Multiset.card_erase_lt_of_mem {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α} :

a ∈ s → ↑Multiset.card (Multiset.erase s a) < ↑Multiset.card s

theorem Multiset.card_erase_le {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α} :

↑Multiset.card (Multiset.erase s a) ≤ ↑Multiset.card s

theorem Multiset.card_erase_eq_ite {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α} :

↑Multiset.card (Multiset.erase s a) = if a ∈ s then Nat.pred (↑Multiset.card s) else ↑Multiset.card s

@[simp]

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

↑(List.reverse l) = ↑l

`Multiset.map` #

def Multiset.map {α : Type u_1} {β : Type u_2} (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.map f l)) (_ : ∀ (_l₁ _l₂ : List α), Setoid.r _l₁ _l₂ → Quot.mk Setoid.r (List.map f _l₁) = Quot.mk Setoid.r (List.map f _l₂))

theorem Multiset.map_congr {α : Type u_1} {β : Type u_2} {f : α → β} {g : α → β} {s : Multiset α} {t : Multiset α} :

s = t → (∀ (x : α), x ∈ t → f x = g x) → Multiset.map f s = Multiset.map g t

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

HEq (Multiset.map f m) (Multiset.map f' m)

theorem Multiset.forall_mem_map_iff {α : Type u_1} {β : Type u_2} {f : α → β} {p : β → Prop} {s : Multiset α} :

((y : β) → y ∈ Multiset.map f s → p y) ↔ (x : α) → x ∈ s → p (f x)

@[simp]

theorem Multiset.coe_map {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) :

Multiset.map f ↑l = ↑(List.map f l)

@[simp]

theorem Multiset.map_zero {α : Type u_2} {β : Type u_1} (f : α → β) :

Multiset.map f 0 = 0

@[simp]

theorem Multiset.map_cons {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) (s : Multiset α) :

Multiset.map f (a ::ₘ s) = f a ::ₘ Multiset.map f s

theorem Multiset.map_comp_cons {α : Type u_1} {β : Type u_2} (f : α → β) (t : α) :

Multiset.map f ∘ Multiset.cons t = Multiset.cons (f t) ∘ Multiset.map f

@[simp]

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

Multiset.map f {a} = {f a}

@[simp]

theorem Multiset.map_replicate {α : Type u_2} {β : Type u_1} (f : α → β) (k : ℕ) (a : α) :

Multiset.map f (Multiset.replicate k a) = Multiset.replicate k (f a)

@[simp]

theorem Multiset.map_add {α : Type u_1} {β : Type u_2} (f : α → β) (s : Multiset α) (t : Multiset α) :

Multiset.map f (s + t) = Multiset.map f s + Multiset.map f t

instance Multiset.canLift {α : Type u_1} {β : Type u_2} (c : β → α) (p : α → Prop) [inst : CanLift α β c p] :

CanLift (Multiset α) (Multiset β) (Multiset.map c) fun s => (x : α) → x ∈ s → p x

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

Equations

Multiset.canLift c p = { prf := (_ : ∀ (x : Multiset α), ((x_1 : α) → x_1 ∈ x → p x_1) → ∃ y, Multiset.map c y = x) }

def Multiset.mapAddMonoidHom {α : Type u_1} {β : Type u_2} (f : α → β) :

Multiset α →+ Multiset β

Multiset.map as an AddMonoidHom.

Equations

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

@[simp]

theorem Multiset.coe_mapAddMonoidHom {α : Type u_1} {β : Type u_2} (f : α → β) :

↑(Multiset.mapAddMonoidHom f) = Multiset.map f

theorem Multiset.map_nsmul {α : Type u_1} {β : Type u_2} (f : α → β) (n : ℕ) (s : Multiset α) :

Multiset.map f (n • s) = n • Multiset.map f s

@[simp]

theorem Multiset.mem_map {α : Type u_1} {β : Type u_2} {f : α → β} {b : β} {s : Multiset α} :

b ∈ Multiset.map f s ↔ ∃ a, a ∈ s ∧ f a = b

@[simp]

theorem Multiset.card_map {α : Type u_1} {β : Type u_2} (f : α → β) (s : Multiset α) :

↑Multiset.card (Multiset.map f s) = ↑Multiset.card s

@[simp]

theorem Multiset.map_eq_zero {α : Type u_1} {β : Type u_2} {s : Multiset α} {f : α → β} :

Multiset.map f s = 0 ↔ s = 0

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

f a ∈ Multiset.map f s

theorem Multiset.map_eq_singleton {α : Type u_1} {β : Type u_2} {f : α → β} {s : Multiset α} {b : β} :

Multiset.map f s = {b} ↔ ∃ a, s = {a} ∧ f a = b

theorem Multiset.map_eq_cons {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] (f : α → β) (s : Multiset α) (t : Multiset β) (b : β) :

(∃ a, a ∈ s ∧ f a = b ∧ Multiset.map f (Multiset.erase s a) = t) ↔ Multiset.map f s = b ::ₘ t

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

f a ∈ Multiset.map f s ↔ a ∈ s

@[simp]

theorem Multiset.map_map {α : Type u_1} {β : Type u_3} {γ : Type u_2} (g : β → γ) (f : α → β) (s : Multiset α) :

Multiset.map g (Multiset.map f s) = Multiset.map (g ∘ f) s

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

Multiset.map id s = s

@[simp]

theorem Multiset.map_id' {α : Type u_1} (s : Multiset α) :

Multiset.map (fun x => x) s = s

theorem Multiset.map_const {α : Type u_1} {β : Type u_2} (s : Multiset α) (b : β) :

Multiset.map (Function.const α b) s = Multiset.replicate (↑Multiset.card s) b

@[simp]

theorem Multiset.map_const' {α : Type u_1} {β : Type u_2} (s : Multiset α) (b : β) :

Multiset.map (fun x => b) s = Multiset.replicate (↑Multiset.card s) b

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

b₁ = b₂

@[simp]

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

Multiset.map f s ≤ Multiset.map f t

@[simp]

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

Multiset.map f s < Multiset.map f t

theorem Multiset.map_mono {α : Type u_1} {β : Type u_2} (f : α → β) :

Monotone (Multiset.map f)

theorem Multiset.map_strictMono {α : Type u_1} {β : Type u_2} (f : α → β) :

StrictMono (Multiset.map f)

@[simp]

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

Multiset.map f s ⊆ Multiset.map f t

theorem Multiset.map_erase {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst : DecidableEq β] (f : α → β) (hf : Function.Injective f) (x : α) (s : Multiset α) :

Multiset.map f (Multiset.erase s x) = Multiset.erase (Multiset.map f s) (f x)

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

Function.Surjective (Multiset.map f)

`Multiset.fold` #

def Multiset.foldl {α : Type u_1} {β : Type u_2} (f : β → α → β) (H : 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 H b s = Quot.liftOn s (fun l => List.foldl f b l) (_ : ∀ (_l₁ _l₂ : List α), Setoid.r _l₁ _l₂ → List.foldl f b _l₁ = List.foldl f b _l₂)

@[simp]

theorem Multiset.foldl_zero {α : Type u_1} {β : Type u_2} (f : β → α → β) (H : RightCommutative f) (b : β) :

Multiset.foldl f H b 0 = b

@[simp]

theorem Multiset.foldl_cons {α : Type u_1} {β : Type u_2} (f : β → α → β) (H : RightCommutative f) (b : β) (a : α) (s : Multiset α) :

Multiset.foldl f H b (a ::ₘ s) = Multiset.foldl f H (f b a) s

@[simp]

theorem Multiset.foldl_add {α : Type u_1} {β : Type u_2} (f : β → α → β) (H : RightCommutative f) (b : β) (s : Multiset α) (t : Multiset α) :

Multiset.foldl f H b (s + t) = Multiset.foldl f H (Multiset.foldl f H b s) t

def Multiset.foldr {α : Type u_1} {β : Type u_2} (f : α → β → β) (H : 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 H b s = Quot.liftOn s (fun l => List.foldr f b l) (_ : ∀ (_l₁ _l₂ : List α), Setoid.r _l₁ _l₂ → List.foldr f b _l₁ = List.foldr f b _l₂)

@[simp]

theorem Multiset.foldr_zero {α : Type u_1} {β : Type u_2} (f : α → β → β) (H : LeftCommutative f) (b : β) :

Multiset.foldr f H b 0 = b

@[simp]

theorem Multiset.foldr_cons {α : Type u_1} {β : Type u_2} (f : α → β → β) (H : LeftCommutative f) (b : β) (a : α) (s : Multiset α) :

Multiset.foldr f H b (a ::ₘ s) = f a (Multiset.foldr f H b s)

@[simp]

theorem Multiset.foldr_singleton {α : Type u_1} {β : Type u_2} (f : α → β → β) (H : LeftCommutative f) (b : β) (a : α) :

Multiset.foldr f H b {a} = f a b

@[simp]

theorem Multiset.foldr_add {α : Type u_1} {β : Type u_2} (f : α → β → β) (H : LeftCommutative f) (b : β) (s : Multiset α) (t : Multiset α) :

Multiset.foldr f H b (s + t) = Multiset.foldr f H (Multiset.foldr f H b t) s

@[simp]

theorem Multiset.coe_foldr {α : Type u_1} {β : Type u_2} (f : α → β → β) (H : LeftCommutative f) (b : β) (l : List α) :

Multiset.foldr f H b ↑l = List.foldr f b l

@[simp]

theorem Multiset.coe_foldl {α : Type u_1} {β : Type u_2} (f : β → α → β) (H : RightCommutative f) (b : β) (l : List α) :

Multiset.foldl f H b ↑l = List.foldl f b l

theorem Multiset.coe_foldr_swap {α : Type u_1} {β : Type u_2} (f : α → β → β) (H : LeftCommutative f) (b : β) (l : List α) :

Multiset.foldr f H b ↑l = List.foldl (fun x y => f y x) b l

theorem Multiset.foldr_swap {α : Type u_1} {β : Type u_2} (f : α → β → β) (H : LeftCommutative f) (b : β) (s : Multiset α) :

Multiset.foldr f H b s = Multiset.foldl (fun x y => f y x) (_ : ∀ (_x : β) (_y _z : α), f _z (f _y _x) = f _y (f _z _x)) b s

theorem Multiset.foldl_swap {α : Type u_1} {β : Type u_2} (f : β → α → β) (H : RightCommutative f) (b : β) (s : Multiset α) :

Multiset.foldl f H b s = Multiset.foldr (fun x y => f y x) (_ : ∀ (_x _y : α) (_z : β), f (f _z _y) _x = f (f _z _x) _y) b s

theorem Multiset.foldr_induction' {α : Type u_1} {β : Type u_2} (f : α → β → β) (H : 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 : α) → a ∈ s → q a) :

p (Multiset.foldr f H x s)

theorem Multiset.foldr_induction {α : Type u_1} (f : α → α → α) (H : 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 : α) → a ∈ s → p a) :

p (Multiset.foldr f H x s)

theorem Multiset.foldl_induction' {α : Type u_1} {β : Type u_2} (f : β → α → β) (H : 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 : α) → a ∈ s → q a) :

p (Multiset.foldl f H x s)

theorem Multiset.foldl_induction {α : Type u_1} (f : α → α → α) (H : 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 : α) → a ∈ s → p a) :

p (Multiset.foldl f H x s)

Map for partial functions #

def Multiset.pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p a → β) (s : Multiset α) :

((a : α) → 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

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

@[simp]

theorem Multiset.coe_pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p a → β) (l : List α) (H : (a : α) → a ∈ l → p a) :

Multiset.pmap f (↑l) H = ↑(List.pmap f l H)

@[simp]

theorem Multiset.pmap_zero {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p a → β) (h : (a : α) → a ∈ 0 → p a) :

Multiset.pmap f 0 h = 0

@[simp]

theorem Multiset.pmap_cons {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p a → β) (a : α) (m : Multiset α) (h : (b : α) → b ∈ a ::ₘ m → p b) :

Multiset.pmap f (a ::ₘ m) h = f a (h a (_ : a ∈ a ::ₘ m)) ::ₘ Multiset.pmap f m fun a ha => h a (_ : a ∈ a ::ₘ 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

Multiset.attach s = Multiset.pmap Subtype.mk s (_ : ∀ (_a : α), _a ∈ s → _a ∈ s)

@[simp]

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

Multiset.attach ↑l = ↑(List.attach l)

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

sizeOf x < sizeOf s

theorem Multiset.pmap_eq_map {α : Type u_1} {β : Type u_2} (p : α → Prop) (f : α → β) (s : Multiset α) (H : (a : α) → a ∈ s → p a) :

Multiset.pmap (fun a x => f a) s H = Multiset.map f s

theorem Multiset.pmap_congr {α : Type u_1} {β : Type u_2} {p : α → Prop} {q : α → Prop} {f : (a : α) → p a → β} {g : (a : α) → q a → β} (s : Multiset α) {H₁ : (a : α) → a ∈ s → p a} {H₂ : (a : α) → a ∈ s → q a} :

(∀ (a : α), a ∈ s → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂) → Multiset.pmap f s H₁ = Multiset.pmap g s H₂

theorem Multiset.map_pmap {α : Type u_1} {β : Type u_3} {γ : Type u_2} {p : α → Prop} (g : β → γ) (f : (a : α) → p a → β) (s : Multiset α) (H : (a : α) → a ∈ s → p a) :

Multiset.map g (Multiset.pmap f s H) = Multiset.pmap (fun a h => g (f a h)) s H

theorem Multiset.pmap_eq_map_attach {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p a → β) (s : Multiset α) (H : (a : α) → a ∈ s → p a) :

Multiset.pmap f s H = Multiset.map (fun x => f (↑x) (H ↑x (_ : ↑x ∈ s))) (Multiset.attach s)

theorem Multiset.attach_map_val' {α : Type u_1} {β : Type u_2} (s : Multiset α) (f : α → β) :

Multiset.map (fun i => f ↑i) (Multiset.attach s) = Multiset.map f s

@[simp]

theorem Multiset.attach_map_val {α : Type u_1} (s : Multiset α) :

Multiset.map Subtype.val (Multiset.attach s) = s

@[simp]

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

x ∈ Multiset.attach s

@[simp]

theorem Multiset.mem_pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {s : Multiset α} {H : (a : α) → a ∈ s → p a} {b : β} :

b ∈ Multiset.pmap f s H ↔ ∃ a h, f a (H a h) = b

@[simp]

theorem Multiset.card_pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p a → β) (s : Multiset α) (H : (a : α) → a ∈ s → p a) :

↑Multiset.card (Multiset.pmap f s H) = ↑Multiset.card s

@[simp]

theorem Multiset.card_attach {α : Type u_1} {m : Multiset α} :

↑Multiset.card (Multiset.attach m) = ↑Multiset.card m

@[simp]

theorem Multiset.attach_zero {α : Type u_1} :

Multiset.attach 0 = 0

theorem Multiset.attach_cons {α : Type u_1} (a : α) (m : Multiset α) :

Multiset.attach (a ::ₘ m) = { val := a, property := (_ : a ∈ a ::ₘ m) } ::ₘ Multiset.map (fun p => { val := ↑p, property := (_ : ↑p ∈ a ::ₘ m) }) (Multiset.attach m)

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

Decidable ((a : α) → 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 => decidable_of_iff ((a : α) → a ∈ l → p a) (_ : ((a : α) → a ∈ l → p a) ↔ (a : α) → 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

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

instance Multiset.decidableEqPiMultiset {α : Type u_1} {m : Multiset α} {β : α → Type u_2} [h : (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) (_ : (∀ (a : α) (h : a ∈ m), f a h = g a h) ↔ f = g)

def Multiset.decidableExistsMultiset {α : Type u_1} {m : Multiset α} {p : α → Prop} [inst : DecidablePred p] :

Decidable (∃ x, 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 => decidable_of_iff (∃ a, a ∈ l ∧ p a) (_ : (∃ a, a ∈ l ∧ p a) ↔ ∃ x, x ∈ ↑l ∧ p x)

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, p a h)

Equations

Multiset.decidableDexistsMultiset = decidable_of_iff (∃ x, x ∈ Multiset.attach m ∧ p ↑x (_ : ↑x ∈ m)) (_ : (∃ x, x ∈ Multiset.attach m ∧ p ↑x (_ : ↑x ∈ m)) ↔ ∃ a h, p a h)

Subtraction #

def Multiset.sub {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) (t : 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 it is 0 if count a t ≥ count a s).

Equations

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

instance Multiset.instSubMultiset {α : Type u_1} [inst : DecidableEq α] :

Sub (Multiset α)

Equations

Multiset.instSubMultiset = { sub := Multiset.sub }

@[simp]

theorem Multiset.coe_sub {α : Type u_1} [inst : DecidableEq α] (s : List α) (t : List α) :

↑s - ↑t = ↑(List.diff s t)

theorem Multiset.sub_zero {α : Type u_1} [inst : 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} [inst : DecidableEq α] (a : α) (s : Multiset α) (t : Multiset α) :

s - a ::ₘ t = Multiset.erase s a - t

theorem Multiset.sub_le_iff_le_add {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {t : Multiset α} {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 α).

instance Multiset.instOrderedSubMultisetToLEToPreorderInstPartialOrderMultisetInstAddMultisetInstSubMultiset {α : Type u_1} [inst : DecidableEq α] :

OrderedSub (Multiset α)

Equations

Multiset.instOrderedSubMultisetToLEToPreorderInstPartialOrderMultisetInstAddMultisetInstSubMultiset = { tsub_le_iff_right := (_ : ∀ (_n _m _k : Multiset α), _n - _m ≤ _k ↔ _n ≤ _k + _m) }

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

a ::ₘ s - t = a ::ₘ (s - t)

theorem Multiset.sub_eq_fold_erase {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) (t : Multiset α) :

s - t = Multiset.foldl Multiset.erase (_ : ∀ (s : Multiset α) (a b : α), Multiset.erase (Multiset.erase s a) b = Multiset.erase (Multiset.erase s b) a) s t

@[simp]

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

↑Multiset.card (s - t) = ↑Multiset.card s - ↑Multiset.card t

Union #

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

s ∪ t is the lattice join operation with respect to the multiset ≤. The multiplicity of a in s ∪ t is the maximum of the multiplicities in s and t.

Equations

Multiset.union s t = s - t + t

instance Multiset.instUnionMultiset {α : Type u_1} [inst : DecidableEq α] :

Union (Multiset α)

Equations

Multiset.instUnionMultiset = { union := Multiset.union }

theorem Multiset.union_def {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) (t : Multiset α) :

s ∪ t = s - t + t

theorem Multiset.le_union_left {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) (t : Multiset α) :

s ≤ s ∪ t

theorem Multiset.le_union_right {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) (t : Multiset α) :

t ≤ s ∪ t

theorem Multiset.eq_union_left {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {t : Multiset α} :

t ≤ s → s ∪ t = s

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

s ∪ u ≤ t ∪ u

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

s ∪ t ≤ u

@[simp]

theorem Multiset.mem_union {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {t : Multiset α} {a : α} :

a ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t

@[simp]

theorem Multiset.map_union {α : Type u_2} {β : Type u_1} [inst : DecidableEq α] [inst : DecidableEq β] {f : α → β} (finj : Function.Injective f) {s : Multiset α} {t : Multiset α} :

Multiset.map f (s ∪ t) = Multiset.map f s ∪ Multiset.map f t

@[simp]

theorem Multiset.zero_union {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} :

0 ∪ s = s

@[simp]

theorem Multiset.union_zero {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} :

s ∪ 0 = s

Intersection #

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

s ∩ t is the lattice meet operation with respect to the multiset ≤. The multiplicity of a in s ∩ t is the minimum of the multiplicities in s and t.

Equations

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

instance Multiset.instInterMultiset {α : Type u_1} [inst : DecidableEq α] :

Inter (Multiset α)

Equations

Multiset.instInterMultiset = { inter := Multiset.inter }

@[simp]

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

s ∩ 0 = 0

@[simp]

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

0 ∩ s = 0

@[simp]

theorem Multiset.cons_inter_of_pos {α : Type u_1} [inst : DecidableEq α] {a : α} (s : Multiset α) {t : Multiset α} :

a ∈ t → (a ::ₘ s) ∩ t = a ::ₘ s ∩ Multiset.erase t a

@[simp]

theorem Multiset.cons_inter_of_neg {α : Type u_1} [inst : DecidableEq α] {a : α} (s : Multiset α) {t : Multiset α} :

¬a ∈ t → (a ::ₘ s) ∩ t = s ∩ t

theorem Multiset.inter_le_left {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) (t : Multiset α) :

s ∩ t ≤ s

theorem Multiset.inter_le_right {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) (t : Multiset α) :

s ∩ t ≤ t

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

s ≤ t ∩ u

@[simp]

theorem Multiset.mem_inter {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {t : Multiset α} {a : α} :

a ∈ s ∩ t ↔ a ∈ s ∧ a ∈ t

instance Multiset.instLatticeMultiset {α : Type u_1} [inst : DecidableEq α] :

Lattice (Multiset α)

Equations

Multiset.instLatticeMultiset = Lattice.mk (_ : ∀ (s t : Multiset α), s ∩ t ≤ s) (_ : ∀ (s t : Multiset α), s ∩ t ≤ t) (_ : ∀ {s t u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u)

@[simp]

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

s ⊔ t = s ∪ t

@[simp]

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

s ⊓ t = s ∩ t

@[simp]

theorem Multiset.le_inter_iff {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {t : Multiset α} {u : Multiset α} :

s ≤ t ∩ u ↔ s ≤ t ∧ s ≤ u

@[simp]

theorem Multiset.union_le_iff {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {t : Multiset α} {u : Multiset α} :

s ∪ t ≤ u ↔ s ≤ u ∧ t ≤ u

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

s ∪ t = t ∪ s

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

s ∩ t = t ∩ s

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

s ∪ t = t

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

u ∪ s ≤ u ∪ t

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

s ∪ t ≤ s + t

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

s ∪ t + u = s + u ∪ (t + u)

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

s + (t ∪ u) = s + t ∪ (s + u)

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

a ::ₘ (s ∪ t) = a ::ₘ s ∪ a ::ₘ t

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

s ∩ t + u = (s + u) ∩ (t + u)

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

s + t ∩ u = (s + t) ∩ (s + u)

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

a ::ₘ s ∩ t = (a ::ₘ s) ∩ (a ::ₘ t)

theorem Multiset.union_add_inter {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) (t : Multiset α) :

s ∪ t + s ∩ t = s + t

theorem Multiset.sub_add_inter {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) (t : Multiset α) :

s - t + s ∩ t = s

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

s - s ∩ t = s - t

`Multiset.filter` #

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

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

Equations

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

@[simp]

theorem Multiset.coe_filter {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (l : List α) :

Multiset.filter p ↑l = ↑(List.filter (fun b => decide (p b)) l)

@[simp]

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

Multiset.filter p 0 = 0

theorem Multiset.filter_congr {α : Type u_1} {p : α → Prop} {q : α → Prop} [inst : DecidablePred p] [inst : DecidablePred q] {s : Multiset α} :

(∀ (x : α), x ∈ s → (p x ↔ q x)) → Multiset.filter p s = Multiset.filter q s

@[simp]

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

Multiset.filter p (s + t) = Multiset.filter p s + Multiset.filter p t

@[simp]

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

Multiset.filter p s ≤ s

@[simp]

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

Multiset.filter p s ⊆ s

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

Multiset.filter p s ≤ Multiset.filter p t

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

Monotone (Multiset.filter p)

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

Multiset.filter p s ≤ Multiset.filter q s

@[simp]

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

p a → Multiset.filter p (a ::ₘ s) = a ::ₘ Multiset.filter p s

@[simp]

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

¬p a → Multiset.filter p (a ::ₘ s) = Multiset.filter p s

@[simp]

theorem Multiset.mem_filter {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {a : α} {s : Multiset α} :

a ∈ Multiset.filter p s ↔ a ∈ s ∧ p a

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

p a

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

a ∈ s

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

a ∈ Multiset.filter p l

theorem Multiset.filter_eq_self {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Multiset α} :

Multiset.filter p s = s ↔ (a : α) → a ∈ s → p a

theorem Multiset.filter_eq_nil {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Multiset α} :

Multiset.filter p s = 0 ↔ ∀ (a : α), a ∈ s → ¬p a

theorem Multiset.le_filter {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Multiset α} {t : Multiset α} :

s ≤ Multiset.filter p t ↔ s ≤ t ∧ ((a : α) → a ∈ s → p a)

theorem Multiset.filter_cons {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {a : α} (s : Multiset α) :

Multiset.filter p (a ::ₘ s) = (if p a then {a} else 0) + Multiset.filter p s

theorem Multiset.filter_singleton {α : Type u_1} {a : α} (p : α → Prop) [inst : DecidablePred p] :

Multiset.filter p {a} = if p a then {a} else ∅

theorem Multiset.filter_nsmul {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] (s : Multiset α) (n : ℕ) :

Multiset.filter p (n • s) = n • Multiset.filter p s

@[simp]

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

Multiset.filter p (s - t) = Multiset.filter p s - Multiset.filter p t

@[simp]

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

Multiset.filter p (s ∪ t) = Multiset.filter p s ∪ Multiset.filter p t

@[simp]

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

Multiset.filter p (s ∩ t) = Multiset.filter p s ∩ Multiset.filter p t

@[simp]

theorem Multiset.filter_filter {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (q : α → Prop) [inst : DecidablePred q] (s : Multiset α) :

Multiset.filter p (Multiset.filter q s) = Multiset.filter (fun a => p a ∧ q a) s

theorem Multiset.filter_add_filter {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (q : α → Prop) [inst : DecidablePred q] (s : Multiset α) :

Multiset.filter p s + Multiset.filter q s = Multiset.filter (fun a => p a ∨ q a) s + Multiset.filter (fun a => p a ∧ q a) s

theorem Multiset.filter_add_not {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s : Multiset α) :

Multiset.filter p s + Multiset.filter (fun a => ¬p a) s = s

theorem Multiset.map_filter {α : Type u_2} {β : Type u_1} (p : α → Prop) [inst : DecidablePred p] (f : β → α) (s : Multiset β) :

Multiset.filter p (Multiset.map f s) = Multiset.map f (Multiset.filter (p ∘ f) s)

Simultaneously filter and map elements of a multiset #

def Multiset.filterMap {α : Type u_1} {β : Type u_2} (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

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

@[simp]

theorem Multiset.coe_filterMap {α : Type u_2} {β : Type u_1} (f : α → Option β) (l : List α) :

Multiset.filterMap f ↑l = ↑(List.filterMap f l)

@[simp]

theorem Multiset.filterMap_zero {α : Type u_2} {β : Type u_1} (f : α → Option β) :

Multiset.filterMap f 0 = 0

@[simp]

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

Multiset.filterMap f (a ::ₘ s) = Multiset.filterMap f s

@[simp]

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

Multiset.filterMap f (a ::ₘ s) = b ::ₘ Multiset.filterMap f s

theorem Multiset.filterMap_eq_map {α : Type u_1} {β : Type u_2} (f : α → β) :

Multiset.filterMap (some ∘ f) = Multiset.map f

theorem Multiset.filterMap_eq_filter {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] :

Multiset.filterMap (Option.guard p) = Multiset.filter p

theorem Multiset.filterMap_filterMap {α : Type u_3} {β : Type u_1} {γ : Type u_2} (f : α → Option β) (g : β → Option γ) (s : Multiset α) :

Multiset.filterMap g (Multiset.filterMap f s) = Multiset.filterMap (fun x => Option.bind (f x) g) s

theorem Multiset.map_filterMap {α : Type u_2} {β : Type u_1} {γ : Type u_3} (f : α → Option β) (g : β → γ) (s : Multiset α) :

Multiset.map g (Multiset.filterMap f s) = Multiset.filterMap (fun x => Option.map g (f x)) s

theorem Multiset.filterMap_map {α : Type u_2} {β : Type u_3} {γ : Type u_1} (f : α → β) (g : β → Option γ) (s : Multiset α) :

Multiset.filterMap g (Multiset.map f s) = Multiset.filterMap (g ∘ f) s

theorem Multiset.filter_filterMap {α : Type u_2} {β : Type u_1} (f : α → Option β) (p : β → Prop) [inst : DecidablePred p] (s : Multiset α) :

Multiset.filter p (Multiset.filterMap f s) = Multiset.filterMap (fun x => Option.filter (fun b => decide (p b)) (f x)) s

theorem Multiset.filterMap_filter {α : Type u_2} {β : Type u_1} (p : α → Prop) [inst : DecidablePred p] (f : α → Option β) (s : Multiset α) :

Multiset.filterMap f (Multiset.filter p s) = Multiset.filterMap (fun x => if p x then f x else none) s

@[simp]

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

Multiset.filterMap some s = s

@[simp]

theorem Multiset.mem_filterMap {α : Type u_2} {β : Type u_1} (f : α → Option β) (s : Multiset α) {b : β} :

b ∈ Multiset.filterMap f s ↔ ∃ a, a ∈ s ∧ f a = some b

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

Multiset.map g (Multiset.filterMap f s) = s

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

Multiset.filterMap f s ≤ Multiset.filterMap f t

countp #

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

ℕ

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

Equations

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

@[simp]

theorem Multiset.coe_countp {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (l : List α) :

Multiset.countp p ↑l = List.countp (fun b => decide (p b)) l

@[simp]

theorem Multiset.countp_zero {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] :

Multiset.countp p 0 = 0

@[simp]

theorem Multiset.countp_cons_of_pos {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {a : α} (s : Multiset α) :

p a → Multiset.countp p (a ::ₘ s) = Multiset.countp p s + 1

@[simp]

theorem Multiset.countp_cons_of_neg {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {a : α} (s : Multiset α) :

¬p a → Multiset.countp p (a ::ₘ s) = Multiset.countp p s

theorem Multiset.countp_cons {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (b : α) (s : Multiset α) :

Multiset.countp p (b ::ₘ s) = Multiset.countp p s + if p b then 1 else 0

theorem Multiset.countp_eq_card_filter {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s : Multiset α) :

Multiset.countp p s = ↑Multiset.card (Multiset.filter p s)

theorem Multiset.countp_le_card {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s : Multiset α) :

Multiset.countp p s ≤ ↑Multiset.card s

@[simp]

theorem Multiset.countp_add {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s : Multiset α) (t : Multiset α) :

Multiset.countp p (s + t) = Multiset.countp p s + Multiset.countp p t

@[simp]

theorem Multiset.countp_nsmul {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s : Multiset α) (n : ℕ) :

Multiset.countp p (n • s) = n * Multiset.countp p s

theorem Multiset.card_eq_countp_add_countp {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s : Multiset α) :

↑Multiset.card s = Multiset.countp p s + Multiset.countp (fun x => ¬p x) s

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

Multiset α →+ ℕ

countp p, the number of elements of a multiset satisfying p, promoted to an AddMonoidHom.

Equations

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

@[simp]

theorem Multiset.coe_countpAddMonoidHom {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] :

↑(Multiset.countpAddMonoidHom p) = Multiset.countp p

@[simp]

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

Multiset.countp p (s - t) = Multiset.countp p s - Multiset.countp p t

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

Multiset.countp p s ≤ Multiset.countp p t

@[simp]

theorem Multiset.countp_filter {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (q : α → Prop) [inst : DecidablePred q] (s : Multiset α) :

Multiset.countp p (Multiset.filter q s) = Multiset.countp (fun a => p a ∧ q a) s

theorem Multiset.countp_eq_countp_filter_add {α : Type u_1} (s : Multiset α) (p : α → Prop) (q : α → Prop) [inst : DecidablePred p] [inst : DecidablePred q] :

Multiset.countp p s = Multiset.countp p (Multiset.filter q s) + Multiset.countp p (Multiset.filter (fun a => ¬q a) s)

@[simp]

theorem Multiset.countp_True {α : Type u_1} {s : Multiset α} :

Multiset.countp (fun x => True) s = ↑Multiset.card s

@[simp]

theorem Multiset.countp_False {α : Type u_1} {s : Multiset α} :

Multiset.countp (fun x => False) s = 0

theorem Multiset.countp_map {α : Type u_1} {β : Type u_2} (f : α → β) (s : Multiset α) (p : β → Prop) [inst : DecidablePred p] :

Multiset.countp p (Multiset.map f s) = ↑Multiset.card (Multiset.filter (fun a => p (f a)) s)

theorem Multiset.countp_pos {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Multiset α} :

0 < Multiset.countp p s ↔ ∃ a, a ∈ s ∧ p a

theorem Multiset.countp_eq_zero {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Multiset α} :

Multiset.countp p s = 0 ↔ ∀ (a : α), a ∈ s → ¬p a

theorem Multiset.countp_eq_card {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Multiset α} :

Multiset.countp p s = ↑Multiset.card s ↔ (a : α) → a ∈ s → p a

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

0 < Multiset.countp p s

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

Multiset.countp p s = Multiset.countp p' s'

Multiplicity of an element #

def Multiset.count {α : Type u_1} [inst : 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} [inst : DecidableEq α] (a : α) (l : List α) :

Multiset.count a ↑l = List.count a l

@[simp]

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

Multiset.count a 0 = 0

@[simp]

theorem Multiset.count_cons_self {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Multiset α) :

Multiset.count a (a ::ₘ s) = Multiset.count a s + 1

@[simp]

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

Multiset.count a (b ::ₘ s) = Multiset.count a s

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

Multiset.count a s ≤ ↑Multiset.card s

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

s ≤ t → Multiset.count a s ≤ Multiset.count a t

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

Multiset.count a s ≤ Multiset.count a (b ::ₘ s)

theorem Multiset.count_cons {α : Type u_1} [inst : DecidableEq α] (a : α) (b : α) (s : Multiset α) :

Multiset.count a (b ::ₘ s) = Multiset.count a s + if a = b then 1 else 0

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

Multiset.count a {a} = 1

theorem Multiset.count_singleton {α : Type u_1} [inst : DecidableEq α] (a : α) (b : α) :

Multiset.count a {b} = if a = b then 1 else 0

@[simp]

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

Multiset.count a (s + t) = Multiset.count a s + Multiset.count a t

def Multiset.countAddMonoidHom {α : Type u_1} [inst : DecidableEq α] (a : α) :

Multiset α →+ ℕ

count a, the multiplicity of a in a multiset, promoted to an AddMonoidHom.

Equations

Multiset.countAddMonoidHom a = Multiset.countpAddMonoidHom fun x => a = x

@[simp]

theorem Multiset.coe_countAddMonoidHom {α : Type u_1} [inst : DecidableEq α] {a : α} :

↑(Multiset.countAddMonoidHom a) = Multiset.count a

@[simp]

theorem Multiset.count_nsmul {α : Type u_1} [inst : DecidableEq α] (a : α) (n : ℕ) (s : Multiset α) :

Multiset.count a (n • s) = n * Multiset.count a s

theorem Multiset.count_pos {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α} :

0 < Multiset.count a s ↔ a ∈ s

theorem Multiset.one_le_count_iff_mem {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α} :

1 ≤ Multiset.count a s ↔ a ∈ s

@[simp]

theorem Multiset.count_eq_zero_of_not_mem {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α} (h : ¬a ∈ s) :

Multiset.count a s = 0

@[simp]

theorem Multiset.count_eq_zero {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α} :

Multiset.count a s = 0 ↔ ¬a ∈ s

theorem Multiset.count_ne_zero {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α} :

Multiset.count a s ≠ 0 ↔ a ∈ s

theorem Multiset.count_eq_card {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α} :

Multiset.count a s = ↑Multiset.card s ↔ ∀ (x : α), x ∈ s → a = x

@[simp]

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

Multiset.count a (Multiset.replicate n a) = n

theorem Multiset.count_replicate {α : Type u_1} [inst : DecidableEq α] (a : α) (b : α) (n : ℕ) :

Multiset.count a (Multiset.replicate n b) = if a = b then n else 0

@[simp]

theorem Multiset.count_erase_self {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Multiset α) :

Multiset.count a (Multiset.erase s a) = Multiset.count a s - 1

@[simp]

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

Multiset.count a (Multiset.erase s b) = Multiset.count a s

@[simp]

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

Multiset.count a (s - t) = Multiset.count a s - Multiset.count a t

@[simp]

theorem Multiset.count_union {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Multiset α) (t : Multiset α) :

Multiset.count a (s ∪ t) = max (Multiset.count a s) (Multiset.count a t)

@[simp]

theorem Multiset.count_inter {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Multiset α) (t : Multiset α) :

Multiset.count a (s ∩ t) = min (Multiset.count a s) (Multiset.count a t)

theorem Multiset.le_count_iff_replicate_le {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α} {n : ℕ} :

n ≤ Multiset.count a s ↔ Multiset.replicate n a ≤ s

@[simp]

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

Multiset.count a (Multiset.filter p s) = Multiset.count a s

@[simp]

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

Multiset.count a (Multiset.filter p s) = 0

theorem Multiset.count_filter {α : Type u_1} [inst : DecidableEq α] {p : α → Prop} [inst : DecidablePred p] {a : α} {s : Multiset α} :

Multiset.count a (Multiset.filter p s) = if p a then Multiset.count a s else 0

theorem Multiset.ext {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {t : Multiset α} :

s = t ↔ ∀ (a : α), Multiset.count a s = Multiset.count a t

theorem Multiset.ext' {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {t : Multiset α} :

(∀ (a : α), Multiset.count a s = Multiset.count a t) → s = t

@[simp]

theorem Multiset.coe_inter {α : Type u_1} [inst : DecidableEq α] (s : List α) (t : List α) :

↑s ∩ ↑t = ↑(List.bagInter s t)

theorem Multiset.le_iff_count {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {t : Multiset α} :

s ≤ t ↔ ∀ (a : α), Multiset.count a s ≤ Multiset.count a t

instance Multiset.instDistribLatticeMultiset {α : Type u_1} [inst : DecidableEq α] :

DistribLattice (Multiset α)

Equations

Multiset.instDistribLatticeMultiset = DistribLattice.mk (_ : ∀ (s t u : Multiset α), (s ⊔ t) ⊓ (s ⊔ u) ≤ s ⊔ t ⊓ u)

theorem Multiset.count_map {α : Type u_1} {β : Type u_2} (f : α → β) (s : Multiset α) [inst : DecidableEq β] (b : β) :

Multiset.count b (Multiset.map f s) = ↑Multiset.card (Multiset.filter (fun a => b = f a) s)

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

Multiset.count (f x) (Multiset.map f s) = Multiset.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_2} {β : Type u_1} [inst : DecidableEq α] [inst : DecidableEq β] (f : α → β) (s : Multiset α) (hf : Function.Injective f) (x : α) :

Multiset.count (f x) (Multiset.map f s) = Multiset.count x s

Multiset.map f preserves count if f is injective

@[simp]

theorem Multiset.attach_count_eq_count_coe {α : Type u_1} [inst : DecidableEq α] (m : Multiset α) (a : { x // x ∈ m }) :

Multiset.count a (Multiset.attach m) = Multiset.count (↑a) m

theorem Multiset.filter_eq' {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) (b : α) :

Multiset.filter (fun x => x = b) s = Multiset.replicate (Multiset.count b s) b

theorem Multiset.filter_eq {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) (b : α) :

Multiset.filter (Eq b) s = Multiset.replicate (Multiset.count b s) b

@[simp]

theorem Multiset.replicate_inter {α : Type u_1} [inst : DecidableEq α] (n : ℕ) (x : α) (s : Multiset α) :

Multiset.replicate n x ∩ s = Multiset.replicate (min n (Multiset.count x s)) x

@[simp]

theorem Multiset.inter_replicate {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) (n : ℕ) (x : α) :

s ∩ Multiset.replicate n x = Multiset.replicate (min (Multiset.count x s) n) x

theorem Multiset.addHom_ext {α : Type u_2} {β : Type u_1} [inst : AddZeroClass β] ⦃f : Multiset α →+ β⦄ ⦃g : Multiset α →+ β⦄ (h : ∀ (x : α), ↑f {x} = ↑g {x}) :

f = g

@[simp]

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

Multiset.map f s ≤ Multiset.map f t ↔ s ≤ t

@[simp]

theorem Multiset.mapEmbedding_apply {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Multiset α) :

↑(Multiset.mapEmbedding f).toEmbedding s = Multiset.map (↑f) s

def Multiset.mapEmbedding {α : Type u_1} {β : Type u_2} (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) (_ : ∀ (x x_1 : Multiset α), Multiset.map f.toFun x ≤ Multiset.map f.toFun x_1 ↔ x ≤ x_1)

theorem Multiset.count_eq_card_filter_eq {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) (a : α) :

Multiset.count a s = ↑Multiset.card (Multiset.filter (fun x => a = x) s)

@[simp]

theorem Multiset.map_count_True_eq_filter_card {α : Type u_1} (s : Multiset α) (p : α → Prop) [inst : DecidablePred p] :

Multiset.count True (Multiset.map p s) = ↑Multiset.card (Multiset.filter p s)

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.

Lift a relation to `Multiset`s #

theorem Multiset.Rel_iff {α : Type u_1} {β : Type u_2} (r : α → β → Prop) :

∀ (a : Multiset α) (a_1 : Multiset β), Multiset.Rel r a a_1 ↔ a = 0 ∧ a_1 = 0 ∨ Exists fun {a_2} => Exists fun {b} => Exists fun {as} => Exists fun {bs} => r a_2 b ∧ Multiset.Rel r as bs ∧ a = a_2 ::ₘ as ∧ a_1 = b ::ₘ bs

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

Multiset α → Multiset β → Prop

zero: ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop}, Multiset.Rel r 0 0
cons: ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {a : α} {b : β} {as : Multiset α} {bs : Multiset β}, r a b → Multiset.Rel r as bs → Multiset.Rel r (a ::ₘ as) (b ::ₘ bs)

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 betweem elements in s and t following r.

Instances For

theorem Multiset.rel_flip {α : Type u_2} {β : Type u_1} {r : α → β → Prop} {s : Multiset β} {t : Multiset α} :

Multiset.Rel (flip r) s t ↔ Multiset.Rel r t s