directedOn_ge_Ici — Mathlib

English

For any a in a preorder, the ray Ici(a) = { x | x ≥ a } is directed under the reverse order ≥: for all x, y ≥ a there exists z ≥ a with x ≥ z and y ≥ z (take z = a).

Русский

Для любого a в заданном порядке множество Ici(a) = { x | x ≥ a } направлено относительно порядка ≥: для любых x, y ≥ a существует z ≥ a такой, что x ≥ z и y ≥ z (возьмём z = a).

LaTeX

$$$\forall x \in \mathrm{Ici}(a)\, \forall y \in \mathrm{Ici}(a),\; \exists z \in \mathrm{Ici}(a): x \ge z \land y \ge z$$$

Lean4

theorem directedOn_ge_Ici (a : α) : DirectedOn (· ≥ ·) (Ici a) := fun _x hx _y hy ↦ ⟨a, le_rfl, hx, hy⟩

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