directedOn_le_Iic — Mathlib

English

For every b, the set Iic(b) is directed with respect to ≤; that is, for any x, y ≤ b there exists z ≤ b with x ≤ z and y ≤ z.

Русский

Для любого b множество Iic(b) направлено относительно отношения ≤; то есть для любых x, y ≤ b существует z ≤ b с x ≤ z и y ≤ z.

LaTeX

$$$\forall x,y\in Iic(b)\;\exists z\in Iic(b)\; (x \le z) \wedge (y \le z)$$$

Lean4

theorem directedOn_le_Iic (b : α) : DirectedOn (· ≤ ·) (Iic b) := fun _x hx _y hy ↦ ⟨b, le_rfl, hx, hy⟩

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