Ioc — Mathlib

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

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