English
Let a, b be elements of a preorder. Then the closed interval Icc(a, b) is directed with respect to ≤: for any x, y ∈ Icc(a, b) there exists z ∈ Icc(a, b) with x ≤ z and y ≤ z (take z = b).
Русский
Пусть a, b — элементы частичного порядка. Замкнутый интервал Icc(a, b) направлен относительно порядка ≤: для любых x, y ∈ Icc(a, b) существует z ∈ Icc(a, b) такое, что x ≤ z и y ≤ z (возьмём z = b).
LaTeX
$$$\forall x \in \mathrm{Icc}(a,b)\,\forall y \in \mathrm{Icc}(a,b),\; \exists z \in \mathrm{Icc}(a,b): x \le z \land y \le z$$$
Lean4
theorem directedOn_le_Icc (a b : α) : DirectedOn (· ≤ ·) (Icc a b) := fun _x hx _y hy ↦
⟨b, right_mem_Icc.2 <| hx.1.trans hx.2, hx.2, hy.2⟩
