English
For decidable equality on α, the interval between multisets s and t corresponds to the Finset interval between their toDFinsupp representations via an equivalence: Finset.Icc s t equals the mapped Finset.Icc of toDFinsupps.
Русский
Пусть существование разрешимой эквивалентности, тогда интервал между мультсетами соответствует интервалу конечного множества между их представлениями в toDFinsupp через эквивалентность.
LaTeX
$$$\\mathrm{Icc}(s,t) = \\mathrm{Finset}.map\\big(\\mathrm{Multiset}.equivDFinsupp.toEquiv.symm.toEmbedding\\big)\\big( \\mathrm{Finset}.Icc (\\mathrm{toDFinsupp}s) (\\mathrm{toDFinsupp}t) \\big)$$$
Lean4
theorem Icc_eq :
Finset.Icc s t = (Finset.Icc (toDFinsupp s) (toDFinsupp t)).map Multiset.equivDFinsupp.toEquiv.symm.toEmbedding :=
rfl
