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 α] : LocallyFiniteOrder (Multiset α)

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