# 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.instLocallyFiniteOrder {α : Type u_1} [] :
Equations
• One or more equations did not get rendered due to their size.
theorem Multiset.Icc_eq {α : Type u_1} [] (s : ) (t : ) :
= Finset.map Multiset.equivDFinsupp.symm.toEmbedding (Finset.Icc (Multiset.toDFinsupp s) (Multiset.toDFinsupp t))
theorem Multiset.uIcc_eq {α : Type u_1} [] (s : ) (t : ) :
= Finset.map Multiset.equivDFinsupp.symm.toEmbedding (Finset.uIcc (Multiset.toDFinsupp s) (Multiset.toDFinsupp t))
theorem Multiset.card_Icc {α : Type u_1} [] (s : ) (t : ) :
().card = is.toFinset t.toFinset, ( + 1 - )
theorem Multiset.card_Ico {α : Type u_1} [] (s : ) (t : ) :
().card = is.toFinset t.toFinset, ( + 1 - ) - 1
theorem Multiset.card_Ioc {α : Type u_1} [] (s : ) (t : ) :
().card = is.toFinset t.toFinset, ( + 1 - ) - 1
theorem Multiset.card_Ioo {α : Type u_1} [] (s : ) (t : ) :
().card = is.toFinset t.toFinset, ( + 1 - ) - 2
theorem Multiset.card_uIcc {α : Type u_1} [] (s : ) (t : ) :
().card = is.toFinset t.toFinset, ((() - ()).natAbs + 1)
theorem Multiset.card_Iic {α : Type u_1} [] (s : ) :
().card = is.toFinset, ( + 1)