Multiset.card_Icc

theorem Multiset.card_Icc : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), (Finset.Icc s t).card = (s.toFinset ∪ t.toFinset).prod fun i => Multiset.count i t + 1 - Multiset.count i s

This theorem states that for any two multisets `s` and `t` of type `α`, where `α` has a decidable equality, the cardinality of the finite set interval from `s` to `t` (`Finset.Icc s t`) is equal to the product of the difference in the multiplicity of each element `i` in `t` and `s`, plus one, for all `i` in the union of the finsets derived from `s` and `t`. In other words, the size of the interval between `s` and `t` in a finite set is calculated by subtracting the multiplicities of elements in `s` from the multiplicities of the same elements in `t`, adding one to the result, and taking the product over all these results for all elements in both `s` and `t`.

More concisely: For any two multisets `s` and `t` of type `α` with decidable equality, the cardinality of `Finset.Icc s t` is equal to the product of the differences between the multiplicities of each element in `t` and `s`, plus one, over all elements in `s ∪ t`.