Finite intervals of multisets #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file provides the locally_finite_order instance for multiset α and calculates the
cardinality of its finite intervals.
Implementation notes #
We implement the intervals via the intervals on dfinsupp, rather than via filtering
multiset.powerset; this is because (multiset.replicate n x).powerset has 2^n entries not n+1
entries as it contains duplicates. We do not go via finsupp as this would be noncomputable, and
multisets are typically used computationally.
@[protected, instance]
Equations
- multiset.locally_finite_order = locally_finite_order.of_Icc (multiset α) (λ (f g : multiset α), finset.map multiset.equiv_dfinsupp.to_equiv.symm.to_embedding (finset.Icc (⇑multiset.to_dfinsupp f) (⇑multiset.to_dfinsupp g))) multiset.locally_finite_order._proof_1
theorem
multiset.card_Icc
{α : Type u_1}
[decidable_eq α]
(f g : multiset α) :
(finset.Icc f g).card = (f.to_finset ∪ g.to_finset).prod (λ (i : α), multiset.count i g + 1 - multiset.count i f)
theorem
multiset.card_Ico
{α : Type u_1}
[decidable_eq α]
(f g : multiset α) :
(finset.Ico f g).card = (f.to_finset ∪ g.to_finset).prod (λ (i : α), multiset.count i g + 1 - multiset.count i f) - 1
theorem
multiset.card_Ioc
{α : Type u_1}
[decidable_eq α]
(f g : multiset α) :
(finset.Ioc f g).card = (f.to_finset ∪ g.to_finset).prod (λ (i : α), multiset.count i g + 1 - multiset.count i f) - 1
theorem
multiset.card_Ioo
{α : Type u_1}
[decidable_eq α]
(f g : multiset α) :
(finset.Ioo f g).card = (f.to_finset ∪ g.to_finset).prod (λ (i : α), multiset.count i g + 1 - multiset.count i f) - 2
theorem
multiset.card_Iic
{α : Type u_1}
[decidable_eq α]
(f : multiset α) :
(finset.Iic f).card = f.to_finset.prod (λ (i : α), multiset.count i f + 1)