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