English
uIoo(a, b) is the set of elements strictly between a and b, irrespective of their order.
Русский
uIoo(a, b) — множество элементов строго между a и b независимо от их порядка.
LaTeX
$$$ uIoo(a,b) = Ioo(\min(a,b), \max(a,b)) $$$
Lean4
/-- `uIoo a b` is the set of elements lying between `a` and `b`, with `a` and `b` not included.
Note that we define it more generally in a lattice as `Set.Ioo (a ⊓ b) (a ⊔ b)`. In a product type,
`uIoo` corresponds to the bounding box of the two elements. -/
def uIoo (a b : α) : Set α :=
Ioo (a ⊓ b) (a ⊔ b)