Documentation

Mathlib.Data.Multiset.Interval

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.

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))