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 α) (λ (s t : multiset α), finset.map multiset.equiv_dfinsupp.to_equiv.symm.to_embedding (finset.Icc (⇑multiset.to_dfinsupp s) (⇑multiset.to_dfinsupp t))) multiset.locally_finite_order._proof_1
theorem
multiset.card_Icc
{α : Type u_1}
[decidable_eq α]
(s t : multiset α) :
(finset.Icc s t).card = (s.to_finset ∪ t.to_finset).prod (λ (i : α), multiset.count i t + 1 - multiset.count i s)
theorem
multiset.card_Ico
{α : Type u_1}
[decidable_eq α]
(s t : multiset α) :
(finset.Ico s t).card = (s.to_finset ∪ t.to_finset).prod (λ (i : α), multiset.count i t + 1 - multiset.count i s) - 1
theorem
multiset.card_Ioc
{α : Type u_1}
[decidable_eq α]
(s t : multiset α) :
(finset.Ioc s t).card = (s.to_finset ∪ t.to_finset).prod (λ (i : α), multiset.count i t + 1 - multiset.count i s) - 1
theorem
multiset.card_Ioo
{α : Type u_1}
[decidable_eq α]
(s t : multiset α) :
(finset.Ioo s t).card = (s.to_finset ∪ t.to_finset).prod (λ (i : α), multiset.count i t + 1 - multiset.count i s) - 2
theorem
multiset.card_uIcc
{α : Type u_1}
[decidable_eq α]
(s t : multiset α) :
(finset.uIcc s t).card = (s.to_finset ∪ t.to_finset).prod (λ (i : α), (↑(multiset.count i t) - ↑(multiset.count i s)).nat_abs + 1)
theorem
multiset.card_Iic
{α : Type u_1}
[decidable_eq α]
(s : multiset α) :
(finset.Iic s).card = s.to_finset.prod (λ (i : α), multiset.count i s + 1)