mathlib3 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 α] (s t : multiset α) :
(finset.Icc s t).card = (s.to_finset t.to_finset).prod (λ (i : α), multiset.count i t + 1 - multiset.count i s)
theorem multiset.card_Ico {α : Type u_1} [decidable_eq α] (s t : multiset α) :
(finset.Ico s t).card = (s.to_finset t.to_finset).prod (λ (i : α), multiset.count i t + 1 - multiset.count i s) - 1
theorem multiset.card_Ioc {α : Type u_1} [decidable_eq α] (s t : multiset α) :
(finset.Ioc s t).card = (s.to_finset t.to_finset).prod (λ (i : α), multiset.count i t + 1 - multiset.count i s) - 1
theorem multiset.card_Ioo {α : Type u_1} [decidable_eq α] (s t : multiset α) :
(finset.Ioo s t).card = (s.to_finset t.to_finset).prod (λ (i : α), multiset.count i t + 1 - multiset.count i s) - 2
theorem multiset.card_uIcc {α : Type u_1} [decidable_eq α] (s t : multiset α) :
theorem multiset.card_Iic {α : Type u_1} [decidable_eq α] (s : multiset α) :
(finset.Iic s).card = s.to_finset.prod (λ (i : α), multiset.count i s + 1)