Finite intervals of multisets #
This file provides the LocallyFiniteOrder
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.
instance
Multiset.instLocallyFiniteOrderMultisetToPreorderInstPartialOrderMultiset
{α : Type u_1}
[DecidableEq α]
:
theorem
Multiset.Icc_eq
{α : Type u_1}
[DecidableEq α]
(s : Multiset α)
(t : Multiset α)
:
Finset.Icc s t = Finset.map (Equiv.toEmbedding Multiset.equivDFinsupp.symm)
(Finset.Icc (↑Multiset.toDFinsupp s) (↑Multiset.toDFinsupp t))
theorem
Multiset.uIcc_eq
{α : Type u_1}
[DecidableEq α]
(s : Multiset α)
(t : Multiset α)
:
Finset.uIcc s t = Finset.map (Equiv.toEmbedding Multiset.equivDFinsupp.symm)
(Finset.uIcc (↑Multiset.toDFinsupp s) (↑Multiset.toDFinsupp t))
theorem
Multiset.card_Icc
{α : Type u_1}
[DecidableEq α]
(s : Multiset α)
(t : Multiset α)
:
Finset.card (Finset.Icc s t) = Finset.prod (Multiset.toFinset s ∪ Multiset.toFinset t) fun i => Multiset.count i t + 1 - Multiset.count i s
theorem
Multiset.card_Ico
{α : Type u_1}
[DecidableEq α]
(s : Multiset α)
(t : Multiset α)
:
Finset.card (Finset.Ico s t) = (Finset.prod (Multiset.toFinset s ∪ Multiset.toFinset t) fun i => Multiset.count i t + 1 - Multiset.count i s) - 1
theorem
Multiset.card_Ioc
{α : Type u_1}
[DecidableEq α]
(s : Multiset α)
(t : Multiset α)
:
Finset.card (Finset.Ioc s t) = (Finset.prod (Multiset.toFinset s ∪ Multiset.toFinset t) fun i => Multiset.count i t + 1 - Multiset.count i s) - 1
theorem
Multiset.card_Ioo
{α : Type u_1}
[DecidableEq α]
(s : Multiset α)
(t : Multiset α)
:
Finset.card (Finset.Ioo s t) = (Finset.prod (Multiset.toFinset s ∪ Multiset.toFinset t) fun i => Multiset.count i t + 1 - Multiset.count i s) - 2
theorem
Multiset.card_uIcc
{α : Type u_1}
[DecidableEq α]
(s : Multiset α)
(t : Multiset α)
:
Finset.card (Finset.uIcc s t) = Finset.prod (Multiset.toFinset s ∪ Multiset.toFinset t) fun i =>
Int.natAbs (↑(Multiset.count i t) - ↑(Multiset.count i s)) + 1
theorem
Multiset.card_Iic
{α : Type u_1}
[DecidableEq α]
(s : Multiset α)
:
Finset.card (Finset.Iic s) = Finset.prod (Multiset.toFinset s) fun i => Multiset.count i s + 1