# mathlib3documentation

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.

@[protected, instance]
Equations
theorem multiset.Icc_eq {α : Type u_1} [decidable_eq α] (s t : multiset α) :
theorem multiset.uIcc_eq {α : Type u_1} [decidable_eq α] (s t : multiset α) :
theorem multiset.card_Icc {α : Type u_1} [decidable_eq α] (s t : multiset α) :
t).card = (s.to_finset t.to_finset).prod (λ (i : α), + 1 - s)
theorem multiset.card_Ico {α : Type u_1} [decidable_eq α] (s t : multiset α) :
t).card = (s.to_finset t.to_finset).prod (λ (i : α), + 1 - s) - 1
theorem multiset.card_Ioc {α : Type u_1} [decidable_eq α] (s t : multiset α) :
t).card = (s.to_finset t.to_finset).prod (λ (i : α), + 1 - s) - 1
theorem multiset.card_Ioo {α : Type u_1} [decidable_eq α] (s t : multiset α) :
t).card = (s.to_finset t.to_finset).prod (λ (i : α), + 1 - s) - 2
theorem multiset.card_uIcc {α : Type u_1} [decidable_eq α] (s t : multiset α) :
t).card = (s.to_finset t.to_finset).prod (λ (i : α), ( t) - s)).nat_abs + 1)
theorem multiset.card_Iic {α : Type u_1} [decidable_eq α] (s : multiset α) :
(finset.Iic s).card = s.to_finset.prod (λ (i : α), + 1)