directedOn_le_Ioc — Mathlib

English

Let a, b be in a preorder. The half-open interval Ioc(a, b) is directed under ≤: for any x, y ∈ Ioc(a, b), there exists z ∈ Ioc(a, b) with x ≤ z and y ≤ z (take z = b).

Русский

Пусть a, b — элементы частичного порядка. Полуоткрытый интервал Ioc(a, b) направлен относительно ≤: для любых x, y ∈ Ioc(a, b) существует z ∈ Ioc(a, b) такое, что x ≤ z и y ≤ z (возьмём z = b).

LaTeX

$$$\forall x \in \mathrm{Ioc}(a,b)\,\forall y \in \mathrm{Ioc}(a,b),\; \exists z \in \mathrm{Ioc}(a,b): x \le z \land y \le z$$$

Lean4

theorem directedOn_le_Ioc (a b : α) : DirectedOn (· ≤ ·) (Ioc a b) := fun _x hx _y hy ↦
  ⟨b, right_mem_Ioc.2 <| hx.1.trans_le hx.2, hx.2, hy.2⟩

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