English
Let α be a preorder. For any a ∈ α, the left-open ray Ioi(a) consists of all elements strictly greater than a; i.e., Ioi(a) = { x ∈ α | a < x }.
Русский
Пусть α — предпорядок. Для любого a ∈ α луч слева от a задаётся как Ioi(a) = { x ∈ α | a < x } — все элементы, больший чем a.
LaTeX
$$$$ Ioi(a) = \{ x \in \alpha \mid a < x \}. $$$$
Lean4
/-- `Ioi a` is the left-open right-infinite interval $(a, ∞)$. -/
def Ioi (a : α) :=
{x | a < x}