mathlib documentation

data.multiset.interval

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.

theorem multiset.card_Icc {α : Type u_1} [decidable_eq α] (f g : multiset α) :
(finset.Icc f g).card = (f.to_finset g.to_finset).prod (λ (i : α), multiset.count i g + 1 - multiset.count i f)
theorem multiset.card_Ico {α : Type u_1} [decidable_eq α] (f g : multiset α) :
(finset.Ico f g).card = (f.to_finset g.to_finset).prod (λ (i : α), multiset.count i g + 1 - multiset.count i f) - 1
theorem multiset.card_Ioc {α : Type u_1} [decidable_eq α] (f g : multiset α) :
(finset.Ioc f g).card = (f.to_finset g.to_finset).prod (λ (i : α), multiset.count i g + 1 - multiset.count i f) - 1
theorem multiset.card_Ioo {α : Type u_1} [decidable_eq α] (f g : multiset α) :
(finset.Ioo f g).card = (f.to_finset g.to_finset).prod (λ (i : α), multiset.count i g + 1 - multiset.count i f) - 2
theorem multiset.card_Iic {α : Type u_1} [decidable_eq α] (f : multiset α) :
(finset.Iic f).card = f.to_finset.prod (λ (i : α), multiset.count i f + 1)