Ioo — Mathlib

English

For α with a preorder and locally finite order, the multiset Ioo(a,b) is the underlying multiset of Finset.Ioo(a,b).

Русский

Для α с упорядоченным отношением и локально конечным порядком мультимножество Ioo(a,b) является подлежащим Finset.Ioo(a,b).

LaTeX

$$$\forall \alpha\; [\text{Preorder}(\alpha)]\; [\text{LocallyFiniteOrder}(\alpha)]\; (a,b:\alpha),\; \mathrm{Ioo}(a,b) = (\mathrm{Finset.Ioo}(a,b)).\mathrm{val}.$$$

Lean4

/-- The multiset of elements `x` such that `a < x` and `x < b`. Basically `Set.Ioo a b` as a
multiset. -/
def Ioo (a b : α) : Multiset α :=
  (Finset.Ioo a b).val

Похожие утверждения