Multisets #
These are implemented as the quotient of a list by permutations.
Notation #
We define the global infix notation ::ₘ for multiset.cons.
@[protected, instance]
Equations
- multiset.has_coe = {coe := quot.mk setoid.r}
@[simp]
@[protected, instance]
Equations
- multiset.has_decidable_eq s₁ s₂ = quotient.rec_on_subsingleton₂ s₁ s₂ (λ (l₁ l₂ : list α), decidable_of_iff' (l₁ ≈ l₂) _)
@[protected]
defines a size for a multiset by referring to the size of the underlying list
Equations
- s.sizeof = quot.lift_on s sizeof multiset.sizeof._proof_1
@[protected, instance]
Equations
- multiset.has_sizeof = {sizeof := multiset.sizeof _inst_1}
Empty multiset #
@[protected, instance]
Equations
- multiset.has_zero = {zero := multiset.zero α}
@[protected, instance]
Equations
- multiset.has_emptyc = {emptyc := 0}
@[protected, instance]
Equations
cons a s is the multiset which contains s plus one more
instance of a.
@[protected, instance]
Equations
@[protected]
def
multiset.rec
{α : Type u_1}
{C : multiset α → Sort u_4}
(C_0 : C 0)
(C_cons : Π (a : α) (m : multiset α), C m → C (a ::ₘ m))
(C_cons_heq : ∀ (a a' : α) (m : multiset α) (b : C m), 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.hrec_on m (list.rec C_0 (λ (a : α) (l : list α) (b : (λ (l : list α), C ⟦l⟧) l), C_cons a ⟦l⟧ b)) _
@[protected]
def
multiset.rec_on
{α : Type u_1}
{C : multiset α → Sort u_4}
(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), 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.rec_on C_0 C_cons C_cons_heq = multiset.rec C_0 C_cons C_cons_heq m
@[simp]
a ∈ s means that a has nonzero multiplicity in s.
Equations
- multiset.mem a s = quot.lift_on s (λ (l : list α), a ∈ l) _
@[protected, instance]
Equations
- multiset.has_mem = {mem := multiset.mem α}
@[protected, instance]
Equations
@[protected]
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.
@[protected, instance]
Equations
Produces a list of the elements in the multiset using choice.
Equations
- s.to_list = classical.some _
@[protected]
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.lift_on₂ s t list.subperm multiset.le._proof_1
@[protected, instance]
Equations
- multiset.partial_order = {le := multiset.le α, lt := preorder.lt._default multiset.le, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
Singleton #
@[protected, instance]
Equations
- multiset.has_singleton = {singleton := λ (a : α), a ::ₘ 0}
@[protected, instance]
Additive monoid #
@[protected]
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.
@[protected, instance]
Equations
- multiset.has_add = {add := multiset.add α}
@[protected, instance]
Equations
- multiset.ordered_cancel_add_comm_monoid = {add := has_add.add multiset.has_add, add_assoc := _, add_left_cancel := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_cancel_comm_monoid.nsmul._default 0 has_add.add multiset.zero_add multiset.ordered_cancel_add_comm_monoid._proof_3, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := partial_order.le multiset.partial_order, lt := partial_order.lt multiset.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _}
@[protected, instance]
Equations
- multiset.order_bot = {bot := 0, bot_le := _}
@[protected, instance]
Equations
- multiset.canonically_ordered_add_monoid = {add := ordered_cancel_add_comm_monoid.add multiset.ordered_cancel_add_comm_monoid, add_assoc := _, zero := ordered_cancel_add_comm_monoid.zero multiset.ordered_cancel_add_comm_monoid, zero_add := _, add_zero := _, nsmul := ordered_cancel_add_comm_monoid.nsmul multiset.ordered_cancel_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := ordered_cancel_add_comm_monoid.le multiset.ordered_cancel_add_comm_monoid, lt := ordered_cancel_add_comm_monoid.lt multiset.ordered_cancel_add_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, bot := order_bot.bot multiset.order_bot, bot_le := _, le_iff_exists_add := _}
Cardinality #
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 = {to_fun := λ (s : multiset α), quot.lift_on s list.length multiset.card._proof_1, map_zero' := _, map_add' := _}
theorem
multiset.card_add
{α : Type u_1}
(s 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
theorem
multiset.card_eq_one
{α : Type u_1}
{s : multiset α} :
⇑multiset.card s = 1 ↔ ∃ (a : α), s = {a}
theorem
multiset.eq_of_le_of_card_le
{α : Type u_1}
{s t : multiset α}
(h : s ≤ t) :
⇑multiset.card t ≤ ⇑multiset.card s → s = t
@[simp]
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 #
A strong induction principle for multisets: If you construct a value for a particular multiset given values for all strictly smaller multisets, you can construct a value for any multiset.
Equations
- s.strong_induction_on = λ (ih : Π (s : multiset α), (Π (t : multiset α), t < s → p t) → p s), ih s (λ (t : multiset α) (h : t < s), t.strong_induction_on ih)
theorem
multiset.strong_induction_eq
{α : Type u_1}
{p : multiset α → Sort u_2}
(s : multiset α)
(H : Π (s : multiset α), (Π (t : multiset α), t < s → p t) → p s) :
s.strong_induction_on H = H s (λ (t : multiset α) (h : t < s), t.strong_induction_on H)
def
multiset.strong_downward_induction
{α : 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.strong_downward_induction H s = H s (λ (t : multiset α) (ht : ⇑multiset.card t ≤ n) (h : s < t), multiset.strong_downward_induction H t ht)
theorem
multiset.strong_downward_induction_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.strong_downward_induction H s = H s (λ (t : multiset α) (ht : ⇑multiset.card t ≤ n) (hst : s < t), multiset.strong_downward_induction H t ht)
def
multiset.strong_downward_induction_on
{α : 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 strong_downward_induction with order of arguments swapped.
Equations
- multiset.strong_downward_induction_on = λ (s : multiset α) (H : Π (t₁ : multiset α), (Π {t₂ : multiset α}, ⇑multiset.card t₂ ≤ n → t₁ < t₂ → p t₂) → ⇑multiset.card t₁ ≤ n → p t₁), multiset.strong_downward_induction H s
theorem
multiset.strong_downward_induction_on_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₁) :
s.strong_downward_induction_on H = H s (λ (t : multiset α) (ht : ⇑multiset.card t ≤ n) (h : s < t), t.strong_downward_induction_on H ht)
Another way of expressing strong_induction_on: the (<) relation is well-founded.
repeat a n is the multiset containing only a with multiplicity n.
Equations
- multiset.repeat a n = ↑(list.repeat a n)
@[simp]
theorem
multiset.repeat_succ
{α : Type u_1}
(a : α)
(n : ℕ) :
multiset.repeat a (n + 1) = a ::ₘ multiset.repeat a n
@[simp]
theorem
multiset.card_repeat
{α : Type u_1}
(a : α)
(n : ℕ) :
⇑multiset.card (multiset.repeat a n) = n
theorem
multiset.eq_of_mem_repeat
{α : Type u_1}
{a b : α}
{n : ℕ} :
b ∈ multiset.repeat a n → b = a
theorem
multiset.eq_repeat'
{α : Type u_1}
{a : α}
{s : multiset α} :
s = multiset.repeat a (⇑multiset.card s) ↔ ∀ (b : α), b ∈ s → b = a
theorem
multiset.eq_repeat_of_mem
{α : Type u_1}
{a : α}
{s : multiset α} :
(∀ (b : α), b ∈ s → b = a) → s = multiset.repeat a (⇑multiset.card s)
theorem
multiset.eq_repeat
{α : Type u_1}
{a : α}
{n : ℕ}
{s : multiset α} :
s = multiset.repeat a n ↔ ⇑multiset.card s = n ∧ ∀ (b : α), b ∈ s → b = a
theorem
multiset.repeat_le_coe
{α : Type u_1}
{a : α}
{n : ℕ}
{l : list α} :
multiset.repeat a n ≤ ↑l ↔ list.repeat a n <+ l
theorem
multiset.nsmul_repeat
{α : Type u_1}
{a : α}
(n m : ℕ) :
n • multiset.repeat a m = multiset.repeat a (n * m)
Erasing one copy of an element #
erase s a is the multiset that subtracts 1 from the
multiplicity of a.
@[simp]
@[simp]
@[simp]
theorem
multiset.erase_cons_tail
{α : Type u_1}
[decidable_eq α]
{a b : α}
(s : multiset α)
(h : b ≠ a) :
@[simp]
@[simp]
@[simp]
theorem
multiset.mem_erase_of_ne
{α : Type u_1}
[decidable_eq α]
{a b : α}
{s : multiset α}
(ab : a ≠ b) :
theorem
multiset.erase_le_erase
{α : Type u_1}
[decidable_eq α]
{s t : multiset α}
(a : α)
(h : s ≤ t) :
@[simp]
theorem
multiset.card_erase_of_mem
{α : Type u_1}
[decidable_eq α]
{a : α}
{s : multiset α} :
a ∈ s → ⇑multiset.card (s.erase a) = (⇑multiset.card s).pred
@[simp]
theorem
multiset.card_erase_add_one
{α : Type u_1}
[decidable_eq α]
{a : α}
{s : multiset α} :
a ∈ s → ⇑multiset.card (s.erase a) + 1 = ⇑multiset.card s
theorem
multiset.card_erase_lt_of_mem
{α : Type u_1}
[decidable_eq α]
{a : α}
{s : multiset α} :
a ∈ s → ⇑multiset.card (s.erase a) < ⇑multiset.card s
theorem
multiset.card_erase_le
{α : Type u_1}
[decidable_eq α]
{a : α}
{s : multiset α} :
⇑multiset.card (s.erase a) ≤ ⇑multiset.card s
theorem
multiset.card_erase_eq_ite
{α : Type u_1}
[decidable_eq α]
{a : α}
{s : multiset α} :
⇑multiset.card (s.erase a) = ite (a ∈ s) (⇑multiset.card s).pred (⇑multiset.card s)
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.lift_on s (λ (l : list α), ↑(list.map f l)) _
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]
@[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
@[simp]
theorem
multiset.map_singleton
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(a : α) :
multiset.map f {a} = {f a}
theorem
multiset.map_repeat
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(a : α)
(k : ℕ) :
multiset.map f (multiset.repeat a k) = multiset.repeat (f a) k
@[simp]
theorem
multiset.map_add
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(s t : multiset α) :
multiset.map f (s + t) = multiset.map f s + multiset.map f t
@[protected, instance]
If each element of s : multiset α can be lifted to β, then s can be lifted to
multiset β.
Equations
- multiset.can_lift = {coe := multiset.map can_lift.coe, cond := λ (s : multiset α), ∀ (x : α), x ∈ s → can_lift.cond β x, prf := _}
multiset.map as an add_monoid_hom.
Equations
- multiset.map_add_monoid_hom f = {to_fun := multiset.map f, map_zero' := _, map_add' := _}
@[simp]
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]
@[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 : β} :
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_2}
{γ : Type u_3}
(g : β → γ)
(f : α → β)
(s : multiset α) :
multiset.map g (multiset.map f s) = multiset.map (g ∘ f) s
@[simp]
@[simp]
theorem
multiset.map_const
{α : Type u_1}
{β : Type u_2}
(s : multiset α)
(b : β) :
multiset.map (function.const α b) s = multiset.repeat b (⇑multiset.card s)
theorem
multiset.map_congr
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
{s : multiset α} :
(∀ (x : α), x ∈ s → f x = g x) → multiset.map f s = multiset.map g s
theorem
multiset.map_hcongr
{α : Type u_1}
{β β' : Type u_2}
{m : multiset α}
{f : α → β}
{f' : α → β'}
(h : β = β')
(hf : ∀ (a : α), a ∈ m → f a == f' a) :
multiset.map f m == multiset.map f' m
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 t : multiset α}
(h : s ≤ t) :
multiset.map f s ≤ multiset.map f t
@[simp]
theorem
multiset.map_subset_map
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{s t : multiset α}
(H : s ⊆ t) :
multiset.map f s ⊆ multiset.map f t
theorem
multiset.map_erase
{α : Type u_1}
{β : Type u_2}
[decidable_eq α]
[decidable_eq β]
(f : α → β)
(hf : function.injective f)
(x : α)
(s : multiset α) :
multiset.map f (s.erase x) = (multiset.map f s).erase (f x)
def
multiset.foldl
{α : Type u_1}
{β : Type u_2}
(f : β → α → β)
(H : right_commutative 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.lift_on s (λ (l : list α), list.foldl f b l) _
@[simp]
theorem
multiset.foldl_zero
{α : Type u_1}
{β : Type u_2}
(f : β → α → β)
(H : right_commutative f)
(b : β) :
multiset.foldl f H b 0 = b
@[simp]
theorem
multiset.foldl_cons
{α : Type u_1}
{β : Type u_2}
(f : β → α → β)
(H : right_commutative 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 : right_commutative f)
(b : β)
(s 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 : left_commutative 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.lift_on s (λ (l : list α), list.foldr f b l) _
@[simp]
theorem
multiset.foldr_zero
{α : Type u_1}
{β : Type u_2}
(f : α → β → β)
(H : left_commutative f)
(b : β) :
multiset.foldr f H b 0 = b
@[simp]
theorem
multiset.foldr_cons
{α : Type u_1}
{β : Type u_2}
(f : α → β → β)
(H : left_commutative 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 : left_commutative 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 : left_commutative f)
(b : β)
(s 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 : left_commutative 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 : right_commutative 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 : left_commutative f)
(b : β)
(l : list α) :
multiset.foldr f H b ↑l = list.foldl (λ (x : β) (y : α), f y x) b l
theorem
multiset.foldr_swap
{α : Type u_1}
{β : Type u_2}
(f : α → β → β)
(H : left_commutative f)
(b : β)
(s : multiset α) :
multiset.foldr f H b s = multiset.foldl (λ (x : β) (y : α), f y x) _ b s
theorem
multiset.foldl_swap
{α : Type u_1}
{β : Type u_2}
(f : β → α → β)
(H : right_commutative f)
(b : β)
(s : multiset α) :
multiset.foldl f H b s = multiset.foldr (λ (x : α) (y : β), f y x) _ b s
theorem
multiset.foldr_induction'
{α : Type u_1}
{β : Type u_2}
(f : α → β → β)
(H : left_commutative 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 : left_commutative 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 : right_commutative 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 : right_commutative 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)
Sum of a multiset given a commutative additive monoid structure on α.
sum {a, b, c} = a + b + c
Equations
- multiset.sum = multiset.foldr has_add.add multiset.sum._proof_1 0
Product of a multiset given a commutative monoid structure on α.
prod {a, b, c} = a * b * c
Equations
- multiset.prod = multiset.foldr has_mul.mul multiset.prod._proof_1 1
theorem
multiset.sum_eq_foldr
{α : Type u_1}
[add_comm_monoid α]
(s : multiset α) :
s.sum = multiset.foldr has_add.add _ 0 s
theorem
multiset.prod_eq_foldr
{α : Type u_1}
[comm_monoid α]
(s : multiset α) :
s.prod = multiset.foldr has_mul.mul _ 1 s
theorem
multiset.prod_eq_foldl
{α : Type u_1}
[comm_monoid α]
(s : multiset α) :
s.prod = multiset.foldl has_mul.mul _ 1 s
theorem
multiset.sum_eq_foldl
{α : Type u_1}
[add_comm_monoid α]
(s : multiset α) :
s.sum = multiset.foldl has_add.add _ 0 s
@[simp, norm_cast]
@[simp, norm_cast]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
multiset.sum, the sum of the elements of a multiset, promoted to a morphism of
add_comm_monoids.
Equations
- multiset.sum_add_monoid_hom = {to_fun := multiset.sum _inst_1, map_zero' := _, map_add' := _}
@[simp]
@[simp]
theorem
multiset.prod_repeat
{α : Type u_1}
[comm_monoid α]
(a : α)
(n : ℕ) :
(multiset.repeat a n).prod = a ^ n
@[simp]
theorem
multiset.sum_repeat
{α : Type u_1}
[add_comm_monoid α]
(a : α)
(n : ℕ) :
(multiset.repeat a n).sum = n • a
theorem
multiset.sum_map_zero
{α : Type u_1}
{γ : Type u_3}
[add_comm_monoid γ]
{m : multiset α} :
(multiset.map (λ (a : α), 0) m).sum = 0
theorem
multiset.prod_map_one
{α : Type u_1}
{γ : Type u_3}
[comm_monoid γ]
{m : multiset α} :
(multiset.map (λ (a : α), 1) m).prod = 1
@[simp]
theorem
multiset.sum_map_add
{α : Type u_1}
{γ : Type u_3}
[add_comm_monoid γ]
{m : multiset α}
{f g : α → γ} :
(multiset.map (λ (a : α), f a + g a) m).sum = (multiset.map f m).sum + (multiset.map g m).sum
@[simp]
theorem
multiset.prod_map_mul
{α : Type u_1}
{γ : Type u_3}
[comm_monoid γ]
{m : multiset α}
{f g : α → γ} :
(multiset.map (λ (a : α), (f a) * g a) m).prod = ((multiset.map f m).prod) * (multiset.map g m).prod
theorem
multiset.prod_map_prod_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[comm_monoid γ]
(m : multiset α)
(n : multiset β)
{f : α → β → γ} :
(multiset.map (λ (a : α), (multiset.map (λ (b : β), f a b) n).prod) m).prod = (multiset.map (λ (b : β), (multiset.map (λ (a : α), f a b) m).prod) n).prod
theorem
multiset.sum_map_sum_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid γ]
(m : multiset α)
(n : multiset β)
{f : α → β → γ} :
(multiset.map (λ (a : α), (multiset.map (λ (b : β), f a b) n).sum) m).sum = (multiset.map (λ (b : β), (multiset.map (λ (a : α), f a b) m).sum) n).sum
theorem
multiset.sum_map_mul_left
{α : Type u_1}
{β : Type u_2}
[semiring β]
{b : β}
{s : multiset α}
{f : α → β} :
(multiset.map (λ (a : α), b * f a) s).sum = b * (multiset.map f s).sum
theorem
multiset.sum_map_mul_right
{α : Type u_1}
{β : Type u_2}
[semiring β]
{b : β}
{s : multiset α}
{f : α → β} :
(multiset.map (λ (a : α), (f a) * b) s).sum = ((multiset.map f s).sum) * b
theorem
multiset.prod_eq_zero
{M₀ : Type u_1}
[comm_monoid_with_zero M₀]
{s : multiset M₀}
(h : 0 ∈ s) :
theorem
multiset.prod_eq_zero_iff
{M₀ : Type u_1}
[comm_monoid_with_zero M₀]
[no_zero_divisors M₀]
[nontrivial M₀]
{s : multiset M₀} :
theorem
multiset.prod_ne_zero
{M₀ : Type u_1}
[comm_monoid_with_zero M₀]
[no_zero_divisors M₀]
[nontrivial M₀]
{m : multiset M₀}
(h : 0 ∉ m) :
theorem
multiset.sum_hom
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[add_comm_monoid β]
(s : multiset α)
(f : α →+ β) :
theorem
multiset.prod_hom
{α : Type u_1}
{β : Type u_2}
[comm_monoid α]
[comm_monoid β]
(s : multiset α)
(f : α →* β) :
theorem
multiset.sum_hom_rel
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid β]
[add_comm_monoid γ]
(s : multiset α)
{r : β → γ → Prop}
{f : α → β}
{g : α → γ}
(h₁ : r 0 0)
(h₂ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, r b c → r (f a + b) (g a + c)) :
r (multiset.map f s).sum (multiset.map g s).sum
theorem
multiset.prod_hom_rel
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[comm_monoid β]
[comm_monoid γ]
(s : multiset α)
{r : β → γ → Prop}
{f : α → β}
{g : α → γ}
(h₁ : r 1 1)
(h₂ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, r b c → r ((f a) * b) ((g a) * c)) :
r (multiset.map f s).prod (multiset.map g s).prod
@[simp]
@[simp]
theorem
multiset.sum_map_neg
{G : Type u_1}
[add_comm_group G]
(m : multiset G) :
(multiset.map has_neg.neg m).sum = -m.sum
@[simp]
theorem
multiset.prod_map_inv
{G : Type u_1}
[comm_group G]
(m : multiset G) :
(multiset.map has_inv.inv m).prod = (m.prod)⁻¹
theorem
multiset.prod_nonneg
{α : Type u_1}
[ordered_comm_semiring α]
{m : multiset α}
(h : ∀ (a : α), a ∈ m → 0 ≤ a) :
theorem
multiset.prod_le_of_forall_le
{α : Type u_1}
[ordered_comm_monoid α]
(l : multiset α)
(n : α)
(h : ∀ (x : α), x ∈ l → x ≤ n) :
l.prod ≤ n ^ ⇑multiset.card l
theorem
multiset.sum_le_of_forall_le
{α : Type u_1}
[ordered_add_comm_monoid α]
(l : multiset α)
(n : α)
(h : ∀ (x : α), x ∈ l → x ≤ n) :
l.sum ≤ ⇑multiset.card l • n
theorem
multiset.all_one_of_le_one_le_of_prod_eq_one
{α : Type u_1}
[ordered_comm_monoid α]
{m : multiset α} :
theorem
multiset.all_zero_of_le_zero_le_of_sum_eq_zero
{α : Type u_1}
[ordered_add_comm_monoid α]
{m : multiset α} :
theorem
multiset.sum_eq_zero_iff
{α : Type u_1}
[canonically_ordered_add_monoid α]
{m : multiset α} :
theorem
multiset.prod_induction
{M : Type u_1}
[comm_monoid M]
(p : M → Prop)
(s : multiset M)
(p_mul : ∀ (a b : M), p a → p b → p (a * b))
(p_one : p 1)
(p_s : ∀ (a : M), a ∈ s → p a) :
p s.prod
theorem
multiset.sum_induction
{M : Type u_1}
[add_comm_monoid M]
(p : M → Prop)
(s : multiset M)
(p_mul : ∀ (a b : M), p a → p b → p (a + b))
(p_one : p 0)
(p_s : ∀ (a : M), a ∈ s → p a) :
p s.sum
theorem
multiset.le_sum_of_subadditive_on_pred
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[ordered_add_comm_monoid β]
(f : α → β)
(p : α → Prop)
(h_one : f 0 = 0)
(hp_one : p 0)
(h_mul : ∀ (a b : α), p a → p b → f (a + b) ≤ f a + f b)
(hp_mul : ∀ (a b : α), p a → p b → p (a + b))
(s : multiset α)
(hps : ∀ (a : α), a ∈ s → p a) :
f s.sum ≤ (multiset.map f s).sum
theorem
multiset.le_prod_of_submultiplicative_on_pred
{α : Type u_1}
{β : Type u_2}
[comm_monoid α]
[ordered_comm_monoid β]
(f : α → β)
(p : α → Prop)
(h_one : f 1 = 1)
(hp_one : p 1)
(h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ (f a) * f b)
(hp_mul : ∀ (a b : α), p a → p b → p (a * b))
(s : multiset α)
(hps : ∀ (a : α), a ∈ s → p a) :
f s.prod ≤ (multiset.map f s).prod
theorem
multiset.le_prod_of_submultiplicative
{α : Type u_1}
{β : Type u_2}
[comm_monoid α]
[ordered_comm_monoid β]
(f : α → β)
(h_one : f 1 = 1)
(h_mul : ∀ (a b : α), f (a * b) ≤ (f a) * f b)
(s : multiset α) :
f s.prod ≤ (multiset.map f s).prod
theorem
multiset.le_sum_of_subadditive
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[ordered_add_comm_monoid β]
(f : α → β)
(h_one : f 0 = 0)
(h_mul : ∀ (a b : α), f (a + b) ≤ f a + f b)
(s : multiset α) :
f s.sum ≤ (multiset.map f s).sum
theorem
multiset.sum_induction_nonempty
{M : Type u_1}
[add_comm_monoid M]
(p : M → Prop)
(p_mul : ∀ (a b : M), p a → p b → p (a + b))
{s : multiset M}
(hs_nonempty : s ≠ ∅)
(p_s : ∀ (a : M), a ∈ s → p a) :
p s.sum
theorem
multiset.prod_induction_nonempty
{M : Type u_1}
[comm_monoid M]
(p : M → Prop)
(p_mul : ∀ (a b : M), p a → p b → p (a * b))
{s : multiset M}
(hs_nonempty : s ≠ ∅)
(p_s : ∀ (a : M), a ∈ s → p a) :
p s.prod
theorem
multiset.le_prod_nonempty_of_submultiplicative_on_pred
{α : Type u_1}
{β : Type u_2}
[comm_monoid α]
[ordered_comm_monoid β]
(f : α → β)
(p : α → Prop)
(h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ (f a) * f b)
(hp_mul : ∀ (a b : α), p a → p b → p (a * b))
(s : multiset α)
(hs_nonempty : s ≠ ∅)
(hs : ∀ (a : α), a ∈ s → p a) :
f s.prod ≤ (multiset.map f s).prod
theorem
multiset.le_sum_nonempty_of_subadditive_on_pred
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[ordered_add_comm_monoid β]
(f : α → β)
(p : α → Prop)
(h_mul : ∀ (a b : α), p a → p b → f (a + b) ≤ f a + f b)
(hp_mul : ∀ (a b : α), p a → p b → p (a + b))
(s : multiset α)
(hs_nonempty : s ≠ ∅)
(hs : ∀ (a : α), a ∈ s → p a) :
f s.sum ≤ (multiset.map f s).sum
theorem
multiset.le_sum_nonempty_of_subadditive
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[ordered_add_comm_monoid β]
(f : α → β)
(h_mul : ∀ (a b : α), f (a + b) ≤ f a + f b)
(s : multiset α)
(hs_nonempty : s ≠ ∅) :
f s.sum ≤ (multiset.map f s).sum
theorem
multiset.le_prod_nonempty_of_submultiplicative
{α : Type u_1}
{β : Type u_2}
[comm_monoid α]
[ordered_comm_monoid β]
(f : α → β)
(h_mul : ∀ (a b : α), f (a * b) ≤ (f a) * f b)
(s : multiset α)
(hs_nonempty : s ≠ ∅) :
f s.prod ≤ (multiset.map f s).prod
@[simp]
theorem
multiset.sum_map_singleton
{α : Type u_1}
(s : multiset α) :
(multiset.map (λ (a : α), {a}) s).sum = s
theorem
multiset.abs_sum_le_sum_abs
{α : Type u_1}
[linear_ordered_add_comm_group α]
{s : multiset α} :
Join #
join S, where S is a multiset of multisets, is the lift of the list join
operation, that is, the union of all the sets.
join {{1, 2}, {1, 2}, {0, 1}} = {0, 1, 1, 1, 2, 2}
Equations
@[simp]
bind s f is the monad bind operation, defined as join (map f s).
It is the union of f a as a ranges over s.
Equations
- s.bind f = (multiset.map f s).join
@[simp]
@[simp]
@[simp]
@[simp]
theorem
multiset.bind_cons
{α : Type u_1}
{β : Type u_2}
(s : multiset α)
(f : α → β)
(g : α → multiset β) :
@[simp]
theorem
multiset.bind_singleton
{α : Type u_1}
{β : Type u_2}
(s : multiset α)
(f : α → β) :
s.bind (λ (x : α), {f x}) = multiset.map f s
@[simp]
theorem
multiset.card_bind
{α : Type u_1}
{β : Type u_2}
(s : multiset α)
(f : α → multiset β) :
⇑multiset.card (s.bind f) = (multiset.map (⇑multiset.card ∘ f) s).sum
theorem
multiset.map_bind
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(m : multiset α)
(n : α → multiset β)
(f : β → γ) :
multiset.map f (m.bind n) = m.bind (λ (a : α), multiset.map f (n a))
theorem
multiset.bind_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(m : multiset α)
(n : β → multiset γ)
(f : α → β) :
(multiset.map f m).bind n = m.bind (λ (a : α), n (f a))
theorem
multiset.bind_map_comm
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(m : multiset α)
(n : multiset β)
{f : α → β → γ} :
m.bind (λ (a : α), multiset.map (λ (b : β), f a b) n) = n.bind (λ (b : β), multiset.map (λ (a : α), f a b) m)
@[simp]
theorem
multiset.prod_bind
{α : Type u_1}
{β : Type u_2}
[comm_monoid β]
(s : multiset α)
(t : α → multiset β) :
@[simp]
theorem
multiset.sum_bind
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid β]
(s : multiset α)
(t : α → multiset β) :
@[simp]
@[simp]
@[simp]
theorem
multiset.card_product
{α : Type u_1}
{β : Type u_2}
(s : multiset α)
(t : multiset β) :
⇑multiset.card (s.product t) = (⇑multiset.card s) * ⇑multiset.card t
Sigma multiset #
@[protected]
def
multiset.sigma
{α : Type u_1}
{σ : α → Type u_4}
(s : multiset α)
(t : Π (a : α), multiset (σ a)) :
multiset (Σ (a : α), σ a)
sigma s t is the dependent version of product. It is the sum of
(a, b) as a ranges over s and b ranges over t a.
Equations
- s.sigma t = s.bind (λ (a : α), multiset.map (sigma.mk a) (t a))
@[simp]
@[simp]
@[simp]
theorem
multiset.card_sigma
{α : Type u_1}
{σ : α → Type u_4}
(s : multiset α)
(t : Π (a : α), multiset (σ a)) :
⇑multiset.card (s.sigma t) = (multiset.map (λ (a : α), ⇑multiset.card (t a)) s).sum
Map for partial functions #
def
multiset.pmap
{α : Type u_1}
{β : Type u_2}
{p : α → Prop}
(f : Π (a : α), p a → β)
(s : 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.rec_on s (λ (l : list α) (H : ∀ (a : α), a ∈ quot.mk setoid.r l → p a), ↑(list.pmap f l H)) _
@[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 _ ::ₘ multiset.pmap f m _
"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 _
theorem
multiset.sizeof_lt_sizeof_of_mem
{α : Type u_1}
[has_sizeof α]
{x : α}
{s : multiset α}
(hx : x ∈ 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 (λ (a : α) (_x : p a), f a) s H = multiset.map f s
theorem
multiset.pmap_congr
{α : Type u_1}
{β : Type u_2}
{p q : α → Prop}
{f : Π (a : α), p a → β}
{g : Π (a : α), q a → β}
(s : multiset α)
{H₁ : ∀ (a : α), a ∈ s → p a}
{H₂ : ∀ (a : α), a ∈ s → q a}
(h : ∀ (a : α) (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_2}
{γ : Type u_3}
{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 (λ (a : α) (h : p a), 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 (λ (x : {x // x ∈ s}), f x.val _) s.attach
@[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 : a ∈ s), f a _ = 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]
@[protected]
def
multiset.decidable_forall_multiset
{α : Type u_1}
{m : multiset α}
{p : α → Prop}
[hp : Π (a : α), decidable (p a)] :
If p is a decidable predicate,
so is the predicate that all elements of a multiset satisfy p.
Equations
- multiset.decidable_forall_multiset = quotient.rec_on_subsingleton m (λ (l : list α), decidable_of_iff (∀ (a : α), a ∈ l → p a) _)
@[protected, instance]
def
multiset.decidable_dforall_multiset
{α : Type u_1}
{m : multiset α}
{p : Π (a : α), a ∈ m → Prop}
[hp : Π (a : α) (h : a ∈ m), decidable (p a h)] :
Equations
- multiset.decidable_dforall_multiset = decidable_of_decidable_of_iff multiset.decidable_forall_multiset multiset.decidable_dforall_multiset._proof_3
@[protected, instance]
def
multiset.decidable_eq_pi_multiset
{α : Type u_1}
{m : multiset α}
{β : α → Type u_2}
[h : Π (a : α), decidable_eq (β a)] :
decidable_eq (Π (a : α), a ∈ m → β a)
decidable equality for functions whose domain is bounded by multisets
Equations
- multiset.decidable_eq_pi_multiset = λ (f g : Π (a : α), a ∈ m → β a), decidable_of_iff (∀ (a : α) (h : a ∈ m), f a h = g a h) _
def
multiset.decidable_exists_multiset
{α : Type u_1}
{m : multiset α}
{p : α → Prop}
[decidable_pred p] :
If p is a decidable predicate,
so is the existence of an element in a multiset satisfying p.
@[protected, instance]
def
multiset.decidable_dexists_multiset
{α : Type u_1}
{m : multiset α}
{p : Π (a : α), a ∈ m → Prop}
[hp : Π (a : α) (h : a ∈ m), decidable (p a h)] :
Equations
- multiset.decidable_dexists_multiset = decidable_of_decidable_of_iff multiset.decidable_exists_multiset multiset.decidable_dexists_multiset._proof_3
Subtraction #
@[protected]
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).
@[protected, instance]
Equations
- multiset.has_sub = {sub := multiset.sub (λ (a b : α), _inst_1 a b)}
@[simp]
@[protected]
This is a special case of tsub_zero, which should be used instead of this.
This is needed to prove has_ordered_sub (multiset α).
@[simp]
@[protected]
This is a special case of tsub_le_iff_right, which should be used instead of this.
This is needed to prove has_ordered_sub (multiset α).
@[protected, instance]
Equations
@[simp]
theorem
multiset.card_sub
{α : Type u_1}
[decidable_eq α]
{s t : multiset α}
(h : t ≤ s) :
⇑multiset.card (s - t) = ⇑multiset.card s - ⇑multiset.card t
Union #
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.
@[protected, instance]
Equations
- multiset.has_union = {union := multiset.union (λ (a b : α), _inst_1 a b)}
theorem
multiset.union_le_union_right
{α : Type u_1}
[decidable_eq α]
{s t : multiset α}
(h : s ≤ t)
(u : multiset α) :
theorem
multiset.union_le
{α : Type u_1}
[decidable_eq α]
{s t u : multiset α}
(h₁ : s ≤ u)
(h₂ : t ≤ u) :
@[simp]
@[simp]
theorem
multiset.map_union
{α : Type u_1}
{β : Type u_2}
[decidable_eq α]
[decidable_eq β]
{f : α → β}
(finj : function.injective f)
{s t : multiset α} :
multiset.map f (s ∪ t) = multiset.map f s ∪ multiset.map f t
Intersection #
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.
@[protected, instance]
Equations
- multiset.has_inter = {inter := multiset.inter (λ (a b : α), _inst_1 a b)}
@[simp]
@[simp]
@[simp]
theorem
multiset.cons_inter_of_neg
{α : Type u_1}
[decidable_eq α]
{a : α}
(s : multiset α)
{t : multiset α} :
theorem
multiset.le_inter
{α : Type u_1}
[decidable_eq α]
{s t u : multiset α}
(h₁ : s ≤ t)
(h₂ : s ≤ u) :
@[simp]
@[protected, instance]
Equations
- multiset.lattice = {sup := has_union.union multiset.has_union, le := partial_order.le multiset.partial_order, lt := partial_order.lt multiset.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inter.inter multiset.has_inter, inf_le_left := _, inf_le_right := _, le_inf := _}
@[simp]
@[simp]
@[simp]
@[simp]
theorem
multiset.union_le_union_left
{α : Type u_1}
[decidable_eq α]
{s t : multiset α}
(h : s ≤ t)
(u : 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.lift_on s (λ (l : list α), ↑(list.filter p l)) _
@[simp]
theorem
multiset.coe_filter
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(l : list α) :
multiset.filter p ↑l = ↑(list.filter p l)
@[simp]
theorem
multiset.filter_zero
{α : Type u_1}
(p : α → Prop)
[decidable_pred p] :
multiset.filter p 0 = 0
theorem
multiset.filter_congr
{α : Type u_1}
{p q : α → Prop}
[decidable_pred p]
[decidable_pred 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)
[decidable_pred p]
(s 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)
[decidable_pred p]
(s : multiset α) :
multiset.filter p s ≤ s
@[simp]
theorem
multiset.filter_subset
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(s : multiset α) :
multiset.filter p s ⊆ s
theorem
multiset.filter_le_filter
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
{s t : multiset α}
(h : s ≤ t) :
multiset.filter p s ≤ multiset.filter p t
theorem
multiset.monotone_filter_right
{α : Type u_1}
(s : multiset α)
⦃p q : α → Prop⦄
[decidable_pred p]
[decidable_pred q]
(h : p ≤ q) :
multiset.filter p s ≤ multiset.filter q s
@[simp]
theorem
multiset.filter_cons_of_pos
{α : Type u_1}
{p : α → Prop}
[decidable_pred 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}
[decidable_pred 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}
[decidable_pred p]
{a : α}
{s : multiset α} :
a ∈ multiset.filter p s ↔ a ∈ s ∧ p a
theorem
multiset.of_mem_filter
{α : Type u_1}
{p : α → Prop}
[decidable_pred p]
{a : α}
{s : multiset α}
(h : a ∈ multiset.filter p s) :
p a
theorem
multiset.mem_of_mem_filter
{α : Type u_1}
{p : α → Prop}
[decidable_pred p]
{a : α}
{s : multiset α}
(h : a ∈ multiset.filter p s) :
a ∈ s
theorem
multiset.mem_filter_of_mem
{α : Type u_1}
{p : α → Prop}
[decidable_pred 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}
[decidable_pred p]
{s : multiset α} :
multiset.filter p s = s ↔ ∀ (a : α), a ∈ s → p a
theorem
multiset.filter_eq_nil
{α : Type u_1}
{p : α → Prop}
[decidable_pred p]
{s : multiset α} :
multiset.filter p s = 0 ↔ ∀ (a : α), a ∈ s → ¬p a
theorem
multiset.filter_cons
{α : Type u_1}
{p : α → Prop}
[decidable_pred p]
{a : α}
(s : multiset α) :
multiset.filter p (a ::ₘ s) = ite (p a) {a} 0 + multiset.filter p s
theorem
multiset.filter_nsmul
{α : Type u_1}
{p : α → Prop}
[decidable_pred p]
(s : multiset α)
(n : ℕ) :
multiset.filter p (n • s) = n • multiset.filter p s
@[simp]
theorem
multiset.filter_sub
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
[decidable_eq α]
(s 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)
[decidable_pred p]
[decidable_eq α]
(s 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)
[decidable_pred p]
[decidable_eq α]
(s 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)
[decidable_pred p]
(q : α → Prop)
[decidable_pred q]
(s : multiset α) :
multiset.filter p (multiset.filter q s) = multiset.filter (λ (a : α), p a ∧ q a) s
theorem
multiset.filter_add_filter
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(q : α → Prop)
[decidable_pred q]
(s : multiset α) :
multiset.filter p s + multiset.filter q s = multiset.filter (λ (a : α), p a ∨ q a) s + multiset.filter (λ (a : α), p a ∧ q a) s
theorem
multiset.filter_add_not
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(s : multiset α) :
multiset.filter p s + multiset.filter (λ (a : α), ¬p a) s = s
theorem
multiset.map_filter
{α : Type u_1}
{β : Type u_2}
(p : α → Prop)
[decidable_pred 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.filter_map
{α : Type u_1}
{β : Type u_2}
(f : α → option β)
(s : multiset α) :
multiset β
filter_map 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.filter_map f s = quot.lift_on s (λ (l : list α), ↑(list.filter_map f l)) _
@[simp]
theorem
multiset.coe_filter_map
{α : Type u_1}
{β : Type u_2}
(f : α → option β)
(l : list α) :
multiset.filter_map f ↑l = ↑(list.filter_map f l)
@[simp]
theorem
multiset.filter_map_zero
{α : Type u_1}
{β : Type u_2}
(f : α → option β) :
multiset.filter_map f 0 = 0
@[simp]
theorem
multiset.filter_map_cons_none
{α : Type u_1}
{β : Type u_2}
{f : α → option β}
(a : α)
(s : multiset α)
(h : f a = none) :
multiset.filter_map f (a ::ₘ s) = multiset.filter_map f s
@[simp]
theorem
multiset.filter_map_cons_some
{α : Type u_1}
{β : Type u_2}
(f : α → option β)
(a : α)
(s : multiset α)
{b : β}
(h : f a = some b) :
multiset.filter_map f (a ::ₘ s) = b ::ₘ multiset.filter_map f s
theorem
multiset.filter_map_eq_map
{α : Type u_1}
{β : Type u_2}
(f : α → β) :
multiset.filter_map (some ∘ f) = multiset.map f
theorem
multiset.filter_map_filter_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → option β)
(g : β → option γ)
(s : multiset α) :
multiset.filter_map g (multiset.filter_map f s) = multiset.filter_map (λ (x : α), (f x).bind g) s
theorem
multiset.map_filter_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → option β)
(g : β → γ)
(s : multiset α) :
multiset.map g (multiset.filter_map f s) = multiset.filter_map (λ (x : α), option.map g (f x)) s
theorem
multiset.filter_map_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β)
(g : β → option γ)
(s : multiset α) :
multiset.filter_map g (multiset.map f s) = multiset.filter_map (g ∘ f) s
theorem
multiset.filter_filter_map
{α : Type u_1}
{β : Type u_2}
(f : α → option β)
(p : β → Prop)
[decidable_pred p]
(s : multiset α) :
multiset.filter p (multiset.filter_map f s) = multiset.filter_map (λ (x : α), option.filter p (f x)) s
theorem
multiset.filter_map_filter
{α : Type u_1}
{β : Type u_2}
(p : α → Prop)
[decidable_pred p]
(f : α → option β)
(s : multiset α) :
multiset.filter_map f (multiset.filter p s) = multiset.filter_map (λ (x : α), ite (p x) (f x) none) s
@[simp]
theorem
multiset.map_filter_map_of_inv
{α : Type u_1}
{β : Type u_2}
(f : α → option β)
(g : β → α)
(H : ∀ (x : α), option.map g (f x) = some x)
(s : multiset α) :
multiset.map g (multiset.filter_map f s) = s
theorem
multiset.filter_map_le_filter_map
{α : Type u_1}
{β : Type u_2}
(f : α → option β)
{s t : multiset α}
(h : s ≤ t) :
multiset.filter_map f s ≤ multiset.filter_map f t
countp #
countp p s counts the number of elements of s (with multiplicity) that
satisfy p.
Equations
- multiset.countp p s = quot.lift_on s (list.countp p) _
@[simp]
theorem
multiset.coe_countp
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(l : list α) :
multiset.countp p ↑l = list.countp p l
@[simp]
theorem
multiset.countp_zero
{α : Type u_1}
(p : α → Prop)
[decidable_pred p] :
multiset.countp p 0 = 0
@[simp]
theorem
multiset.countp_cons_of_pos
{α : Type u_1}
{p : α → Prop}
[decidable_pred 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}
[decidable_pred p]
{a : α}
(s : multiset α) :
¬p a → multiset.countp p (a ::ₘ s) = multiset.countp p s
theorem
multiset.countp_cons
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(b : α)
(s : multiset α) :
multiset.countp p (b ::ₘ s) = multiset.countp p s + ite (p b) 1 0
theorem
multiset.countp_eq_card_filter
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(s : multiset α) :
multiset.countp p s = ⇑multiset.card (multiset.filter p s)
@[simp]
theorem
multiset.countp_add
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(s t : multiset α) :
multiset.countp p (s + t) = multiset.countp p s + multiset.countp p t
countp p, the number of elements of a multiset satisfying p, promoted to an
add_monoid_hom.
Equations
- multiset.countp_add_monoid_hom p = {to_fun := multiset.countp p (λ (a : α), _inst_1 a), map_zero' := _, map_add' := _}
@[simp]
@[simp]
theorem
multiset.countp_sub
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
[decidable_eq α]
{s 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)
[decidable_pred p]
{s t : multiset α}
(h : s ≤ t) :
multiset.countp p s ≤ multiset.countp p t
@[simp]
theorem
multiset.countp_filter
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(q : α → Prop)
[decidable_pred q]
(s : multiset α) :
multiset.countp p (multiset.filter q s) = multiset.countp (λ (a : α), p a ∧ q a) s
theorem
multiset.countp_map
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(s : multiset α)
(p : β → Prop)
[decidable_pred p] :
multiset.countp p (multiset.map f s) = ⇑multiset.card (multiset.filter (λ (a : α), p (f a)) s)
theorem
multiset.countp_pos
{α : Type u_1}
{p : α → Prop}
[decidable_pred p]
{s : multiset α} :
0 < multiset.countp p s ↔ ∃ (a : α) (H : a ∈ s), p a
theorem
multiset.countp_pos_of_mem
{α : Type u_1}
{p : α → Prop}
[decidable_pred p]
{s : multiset α}
{a : α}
(h : a ∈ s)
(pa : p a) :
0 < multiset.countp p s
Multiplicity of an element #
count a s is the multiplicity of a in s.
Equations
- multiset.count a = multiset.countp (eq a)
@[simp]
theorem
multiset.coe_count
{α : Type u_1}
[decidable_eq α]
(a : α)
(l : list α) :
multiset.count a ↑l = list.count a l
@[simp]
@[simp]
theorem
multiset.count_cons_self
{α : Type u_1}
[decidable_eq α]
(a : α)
(s : multiset α) :
multiset.count a (a ::ₘ s) = (multiset.count a s).succ
@[simp]
theorem
multiset.count_cons_of_ne
{α : Type u_1}
[decidable_eq α]
{a b : α}
(h : a ≠ b)
(s : multiset α) :
multiset.count a (b ::ₘ s) = multiset.count a s
theorem
multiset.count_le_of_le
{α : Type u_1}
[decidable_eq α]
(a : α)
{s t : multiset α} :
s ≤ t → multiset.count a s ≤ multiset.count a t
theorem
multiset.count_le_count_cons
{α : Type u_1}
[decidable_eq α]
(a b : α)
(s : multiset α) :
multiset.count a s ≤ multiset.count a (b ::ₘ s)
theorem
multiset.count_cons
{α : Type u_1}
[decidable_eq α]
(a b : α)
(s : multiset α) :
multiset.count a (b ::ₘ s) = multiset.count a s + ite (a = b) 1 0
theorem
multiset.count_singleton_self
{α : Type u_1}
[decidable_eq α]
(a : α) :
multiset.count a {a} = 1
theorem
multiset.count_singleton
{α : Type u_1}
[decidable_eq α]
(a b : α) :
multiset.count a {b} = ite (a = b) 1 0
@[simp]
theorem
multiset.count_add
{α : Type u_1}
[decidable_eq α]
(a : α)
(s t : multiset α) :
multiset.count a (s + t) = multiset.count a s + multiset.count a t
count a, the multiplicity of a in a multiset, promoted to an add_monoid_hom.
Equations
@[simp]
@[simp]
theorem
multiset.count_nsmul
{α : Type u_1}
[decidable_eq α]
(a : α)
(n : ℕ)
(s : multiset α) :
multiset.count a (n • s) = n * multiset.count a s
theorem
multiset.count_pos
{α : Type u_1}
[decidable_eq α]
{a : α}
{s : multiset α} :
0 < multiset.count a s ↔ a ∈ s
theorem
multiset.one_le_count_iff_mem
{α : Type u_1}
[decidable_eq α]
{a : α}
{s : multiset α} :
1 ≤ multiset.count a s ↔ a ∈ s
@[simp]
theorem
multiset.count_eq_zero_of_not_mem
{α : Type u_1}
[decidable_eq α]
{a : α}
{s : multiset α}
(h : a ∉ s) :
multiset.count a s = 0
@[simp]
theorem
multiset.count_eq_zero
{α : Type u_1}
[decidable_eq α]
{a : α}
{s : multiset α} :
multiset.count a s = 0 ↔ a ∉ s
theorem
multiset.count_ne_zero
{α : Type u_1}
[decidable_eq α]
{a : α}
{s : multiset α} :
multiset.count a s ≠ 0 ↔ a ∈ s
@[simp]
theorem
multiset.count_repeat_self
{α : Type u_1}
[decidable_eq α]
(a : α)
(n : ℕ) :
multiset.count a (multiset.repeat a n) = n
theorem
multiset.count_repeat
{α : Type u_1}
[decidable_eq α]
(a b : α)
(n : ℕ) :
multiset.count a (multiset.repeat b n) = ite (a = b) n 0
@[simp]
theorem
multiset.count_erase_self
{α : Type u_1}
[decidable_eq α]
(a : α)
(s : multiset α) :
multiset.count a (s.erase a) = (multiset.count a s).pred
@[simp]
theorem
multiset.count_erase_of_ne
{α : Type u_1}
[decidable_eq α]
{a b : α}
(ab : a ≠ b)
(s : multiset α) :
multiset.count a (s.erase b) = multiset.count a s
@[simp]
theorem
multiset.count_sub
{α : Type u_1}
[decidable_eq α]
(a : α)
(s t : multiset α) :
multiset.count a (s - t) = multiset.count a s - multiset.count a t
@[simp]
theorem
multiset.count_union
{α : Type u_1}
[decidable_eq α]
(a : α)
(s t : multiset α) :
multiset.count a (s ∪ t) = max (multiset.count a s) (multiset.count a t)
@[simp]
theorem
multiset.count_inter
{α : Type u_1}
[decidable_eq α]
(a : α)
(s t : multiset α) :
multiset.count a (s ∩ t) = min (multiset.count a s) (multiset.count a t)
theorem
multiset.count_sum
{α : Type u_1}
{β : Type u_2}
[decidable_eq α]
{m : multiset β}
{f : β → multiset α}
{a : α} :
multiset.count a (multiset.map f m).sum = (multiset.map (λ (b : β), multiset.count a (f b)) m).sum
theorem
multiset.count_bind
{α : Type u_1}
{β : Type u_2}
[decidable_eq α]
{m : multiset β}
{f : β → multiset α}
{a : α} :
multiset.count a (m.bind f) = (multiset.map (λ (b : β), multiset.count a (f b)) m).sum
theorem
multiset.le_count_iff_repeat_le
{α : Type u_1}
[decidable_eq α]
{a : α}
{s : multiset α}
{n : ℕ} :
n ≤ multiset.count a s ↔ multiset.repeat a n ≤ s
@[simp]
theorem
multiset.count_filter_of_pos
{α : Type u_1}
[decidable_eq α]
{p : α → Prop}
[decidable_pred 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}
[decidable_eq α]
{p : α → Prop}
[decidable_pred p]
{a : α}
{s : multiset α}
(h : ¬p a) :
multiset.count a (multiset.filter p s) = 0
theorem
multiset.count_filter
{α : Type u_1}
[decidable_eq α]
{p : α → Prop}
[decidable_pred p]
{a : α}
{s : multiset α} :
multiset.count a (multiset.filter p s) = ite (p a) (multiset.count a s) 0
theorem
multiset.ext
{α : Type u_1}
[decidable_eq α]
{s t : multiset α} :
s = t ↔ ∀ (a : α), multiset.count a s = multiset.count a t
@[ext]
theorem
multiset.ext'
{α : Type u_1}
[decidable_eq α]
{s t : multiset α} :
(∀ (a : α), multiset.count a s = multiset.count a t) → s = t
@[simp]
theorem
multiset.le_iff_count
{α : Type u_1}
[decidable_eq α]
{s t : multiset α} :
s ≤ t ↔ ∀ (a : α), multiset.count a s ≤ multiset.count a t
@[protected, instance]
Equations
- multiset.distrib_lattice = {sup := lattice.sup multiset.lattice, le := lattice.le multiset.lattice, lt := lattice.lt multiset.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf multiset.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _}
theorem
multiset.repeat_inf
{α : Type u_1}
[decidable_eq α]
(s : multiset α)
(a : α)
(n : ℕ) :
multiset.repeat a n ⊓ s = multiset.repeat a (min (multiset.count a s) n)
theorem
multiset.count_map
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(s : multiset α)
[decidable_eq β]
(b : β) :
multiset.count b (multiset.map f s) = ⇑multiset.card (multiset.filter (λ (a : α), b = f a) s)
theorem
multiset.count_map_eq_count
{α : Type u_1}
{β : Type u_2}
[decidable_eq α]
[decidable_eq β]
(f : α → β)
(s : multiset α)
(hf : set.inj_on 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_1}
{β : Type u_2}
[decidable_eq α]
[decidable_eq β]
(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
theorem
multiset.filter_eq'
{α : Type u_1}
[decidable_eq α]
(s : multiset α)
(b : α) :
multiset.filter (λ (_x : α), _x = b) s = multiset.repeat b (multiset.count b s)
theorem
multiset.filter_eq
{α : Type u_1}
[decidable_eq α]
(s : multiset α)
(b : α) :
multiset.filter (eq b) s = multiset.repeat b (multiset.count b s)
theorem
multiset.pow_count
{α : Type u_1}
[decidable_eq α]
[comm_monoid α]
{s : multiset α}
(a : α) :
a ^ multiset.count a s = (multiset.filter (eq a) s).prod
- 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.
theorem
multiset.rel_flip
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
{s : multiset β}
{t : multiset α} :
multiset.rel (flip r) s t ↔ multiset.rel r t s
theorem
multiset.rel_refl_of_refl_on
{α : Type u_1}
{m : multiset α}
{r : α → α → Prop} :
(∀ (x : α), x ∈ m → r x x) → multiset.rel r m m
theorem
multiset.rel.mono
{α : Type u_1}
{β : Type u_2}
{r p : α → β → Prop}
{s : multiset α}
{t : multiset β}
(hst : multiset.rel r s t)
(h : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → r a b → p a b) :
multiset.rel p s t
theorem
multiset.rel.add
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
{s : multiset α}
{t : multiset β}
{u : multiset α}
{v : multiset β}
(hst : multiset.rel r s t)
(huv : multiset.rel r u v) :
multiset.rel r (s + u) (t + v)
theorem
multiset.rel_flip_eq
{α : Type u_1}
{s t : multiset α} :
multiset.rel (λ (a b : α), b = a) s t ↔ s = t
@[simp]
theorem
multiset.rel_zero_left
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
{b : multiset β} :
multiset.rel r 0 b ↔ b = 0
@[simp]
theorem
multiset.rel_zero_right
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
{a : multiset α} :
multiset.rel r a 0 ↔ a = 0
theorem
multiset.rel_cons_left
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
{a : α}
{as : multiset α}
{bs : multiset β} :
multiset.rel r (a ::ₘ as) bs ↔ ∃ (b : β) (bs' : multiset β), r a b ∧ multiset.rel r as bs' ∧ bs = b ::ₘ bs'
theorem
multiset.rel_cons_right
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
{as : multiset α}
{b : β}
{bs : multiset β} :
multiset.rel r as (b ::ₘ bs) ↔ ∃ (a : α) (as' : multiset α), r a b ∧ multiset.rel r as' bs ∧ as = a ::ₘ as'
theorem
multiset.rel_add_left
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
{as₀ as₁ : multiset α}
{bs : multiset β} :
multiset.rel r (as₀ + as₁) bs ↔ ∃ (bs₀ bs₁ : multiset β), multiset.rel r as₀ bs₀ ∧ multiset.rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
theorem
multiset.rel_add_right
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
{as : multiset α}
{bs₀ bs₁ : multiset β} :
multiset.rel r as (bs₀ + bs₁) ↔ ∃ (as₀ as₁ : multiset α), multiset.rel r as₀ bs₀ ∧ multiset.rel r as₁ bs₁ ∧ as = as₀ + as₁
theorem
multiset.rel_map_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{r : α → β → Prop}
{s : multiset γ}
{f : γ → α}
{t : multiset β} :
multiset.rel r (multiset.map f s) t ↔ multiset.rel (λ (a : γ) (b : β), r (f a) b) s t
theorem
multiset.rel_map_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{r : α → β → Prop}
{s : multiset α}
{t : multiset γ}
{f : γ → β} :
multiset.rel r s (multiset.map f t) ↔ multiset.rel (λ (a : α) (b : γ), r a (f b)) s t
theorem
multiset.rel_join
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
{s : multiset (multiset α)}
{t : multiset (multiset β)}
(h : multiset.rel (multiset.rel r) s t) :
multiset.rel r s.join t.join
theorem
multiset.rel_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{p : γ → δ → Prop}
{s : multiset α}
{t : multiset β}
{f : α → γ}
{g : β → δ} :
multiset.rel p (multiset.map f s) (multiset.map g t) ↔ multiset.rel (λ (a : α) (b : β), p (f a) (g b)) s t
theorem
multiset.rel_bind
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{r : α → β → Prop}
{p : γ → δ → Prop}
{s : multiset α}
{t : multiset β}
{f : α → multiset γ}
{g : β → multiset δ}
(h : (r ⇒ multiset.rel p) f g)
(hst : multiset.rel r s t) :
multiset.rel p (s.bind f) (t.bind g)
theorem
multiset.card_eq_card_of_rel
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
{s : multiset α}
{t : multiset β}
(h : multiset.rel r s t) :
theorem
multiset.exists_mem_of_rel_of_mem
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
{s : multiset α}
{t : multiset β}
(h : multiset.rel r s t)
{a : α}
(ha : a ∈ s) :
∃ (b : β) (H : 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 : ⇑multiset.card m1 = ⇑multiset.card m2) :
multiset.rel r m1 m2
theorem
multiset.rel_repeat_left
{α : Type u_1}
{m : multiset α}
{a : α}
{r : α → α → Prop}
{n : ℕ} :
multiset.rel r (multiset.repeat a n) m ↔ ⇑multiset.card m = n ∧ ∀ (x : α), x ∈ m → r a x
theorem
multiset.rel_repeat_right
{α : Type u_1}
{m : multiset α}
{a : α}
{r : α → α → Prop}
{n : ℕ} :
multiset.rel r m (multiset.repeat a n) ↔ ⇑multiset.card m = n ∧ ∀ (x : α), x ∈ m → r x a
theorem
multiset.sum_le_sum_of_rel_le
{α : Type u_1}
[ordered_add_comm_monoid α]
{m1 m2 : multiset α}
(h : multiset.rel has_le.le m1 m2) :
theorem
multiset.le_sum_of_mem
{α : Type u_1}
[canonically_ordered_add_monoid α]
{m : multiset α}
{a : α}
(h : a ∈ m) :
theorem
multiset.sum_map_le_sum
{α : Type u_1}
[ordered_add_comm_monoid α]
{m : multiset α}
(f : α → α)
(h : ∀ (x : α), x ∈ m → f x ≤ x) :
(multiset.map f m).sum ≤ m.sum
theorem
multiset.sum_le_sum_map
{α : Type u_1}
[ordered_add_comm_monoid α]
{m : multiset α}
(f : α → α)
(h : ∀ (x : α), x ∈ m → x ≤ f x) :
m.sum ≤ (multiset.map f m).sum
theorem
multiset.card_nsmul_le_sum
{α : Type u_1}
[ordered_add_comm_monoid α]
{b : α}
{m : multiset α}
(h : ∀ (x : α), x ∈ m → b ≤ x) :
⇑multiset.card m • b ≤ m.sum
theorem
multiset.sum_le_card_nsmul
{α : Type u_1}
[ordered_add_comm_monoid α]
{b : α}
{m : multiset α}
(h : ∀ (x : α), x ∈ m → x ≤ b) :
m.sum ≤ ⇑multiset.card m • b
theorem
multiset.map_eq_map
{α : Type u_1}
{β : Type u_2}
{f : α → β}
(hf : function.injective f)
{s t : multiset α} :
multiset.map f s = multiset.map f t ↔ s = t
theorem
multiset.map_injective
{α : Type u_1}
{β : Type u_2}
{f : α → β}
(hf : function.injective f) :
theorem
multiset.map_mk_eq_map_mk_of_rel
{α : Type u_1}
{r : α → α → Prop}
{s t : multiset α}
(hst : multiset.rel r s t) :
multiset.map (quot.mk r) s = multiset.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 = multiset.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 (multiset.map (quot.mk r) s)) → p s
Disjoint multisets #
@[simp]
@[simp]
theorem
multiset.disjoint_map_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → γ}
{g : β → γ}
{s : multiset α}
{t : multiset β} :
(multiset.map f s).disjoint (multiset.map g t) ↔ ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → f a ≠ g b
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
theorem
multiset.pairwise_coe_iff_pairwise
{α : Type u_1}
{r : α → α → Prop}
(hr : symmetric r)
{l : list α} :
multiset.pairwise r ↑l ↔ list.pairwise r l
def
multiset.choose_x
{α : Type u_1}
(p : α → Prop)
[decidable_pred 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_x p l hp returns
that a together with proofs of a ∈ l and p a.
Equations
- multiset.choose_x p l = quotient.rec_on l (λ (l' : list α) (ex_unique : ∃! (a : α), a ∈ ⟦l'⟧ ∧ p a), list.choose_x p l' _) _
def
multiset.choose
{α : Type u_1}
(p : α → Prop)
[decidable_pred 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.choose_x p l hp)
theorem
multiset.choose_spec
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(l : multiset α)
(hp : ∃! (a : α), a ∈ l ∧ p a) :
multiset.choose p l hp ∈ l ∧ p (multiset.choose p l hp)
theorem
multiset.choose_mem
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(l : multiset α)
(hp : ∃! (a : α), a ∈ l ∧ p a) :
multiset.choose p l hp ∈ l
theorem
multiset.choose_property
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(l : multiset α)
(hp : ∃! (a : α), a ∈ l ∧ p a) :
p (multiset.choose p l hp)
The equivalence between lists and multisets of a subsingleton type.
Equations
- multiset.subsingleton_equiv α = {to_fun := coe coe_to_lift, inv_fun := quot.lift id _, left_inv := _, right_inv := _}
@[simp]
theorem
monoid_hom.map_multiset_prod
{α : Type u_1}
{β : Type u_2}
[comm_monoid α]
[comm_monoid β]
(f : α →* β)
(s : multiset α) :
theorem
add_monoid_hom.map_multiset_sum
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[add_comm_monoid β]
(f : α →+ β)
(s : multiset α) :