English
The open-closed unordered interval uIoc(a,b) is defined as the ordinary open-closed interval with the smaller endpoint as the left bound and the larger as the right bound.
Русский
Неупорядоченный открыто-закрытый интервал uIoc(a,b) определяется как обычный открыто-закрытый интервал с меньшей границей слева и большей — справа.
LaTeX
$$$ \\mathrm{uIoc}(a,b) := Ioc(\\min(a,b), \\max(a,b)) $$$
Lean4
/-- The open-closed uIcc with unordered bounds. -/
def uIoc : α → α → Set α := fun a b =>
Ioc (min a b)
(max a b)
-- Below is a capital iota