directedOn_ge_Ico — Mathlib

English

In a preorder, the half-open interval Ico(a, b) is directed with respect to ≥: for any x, y ∈ Ico(a, b), there exists z ∈ Ico(a, b) with z ≤ x and z ≤ y (take z = a).

Русский

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

LaTeX

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

Lean4

theorem directedOn_ge_Ico (a b : α) : DirectedOn (· ≥ ·) (Ico a b) := fun _x hx _y hy ↦
  ⟨a, left_mem_Ico.2 <| hx.1.trans_lt hx.2, hx.1, hy.1⟩

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