English
For any α with a preorder and locally finite order, the multiset Icc(a,b) is obtained by taking the underlying multiset of Finset.Icc(a,b).
Русский
Для любого α с упорядоченным отношением и локально конечным порядком множество Icc(a,b) представляет собой мультимножество множества Finset.Icc(a,b).
LaTeX
$$$\forall \alpha\; [\text{Preorder}(\alpha)]\; [\text{LocallyFiniteOrder}(\alpha)]\; (a,b:\alpha),\; \mathrm{Icc}(a,b) = (\mathrm{Finset.Icc}(a,b)).\mathrm{val}.$$$
Lean4
/-- The multiset of elements `x` such that `a ≤ x` and `x ≤ b`. Basically `Set.Icc a b` as a
multiset. -/
def Icc (a b : α) : Multiset α :=
(Finset.Icc a b).val
