Ioi — Mathlib

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}

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