directedOn_ge_Icc — Mathlib

English

In a preorder, the closed interval Icc(a, b) is directed with respect to the reversed order ≥: for any x, y ∈ Icc(a, b) there exists z ∈ Icc(a, b) with z ≤ x and z ≤ y (take z = a).

Русский

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

LaTeX

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

Lean4

theorem directedOn_ge_Icc (a b : α) : DirectedOn (· ≥ ·) (Icc a b) := fun _x hx _y hy ↦
  ⟨a, left_mem_Icc.2 <| hx.1.trans hx.2, hx.1, hy.1⟩

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