exists_le_le — Mathlib

English

In a poset directed under ≥, any two elements a,b have a common lower bound c with c ≤ a and c ≤ b.

Русский

В частично упорядоченном множестве, направленном относительно ≥, для любых a, b существует общий нижний предел c, такой что c ≤ a и c ≤ b.

LaTeX

$$$\forall a,b \in A\;\exists c \in A:\ c \le a \land c \le b$$$

Lean4

theorem exists_le_le [LE α] [IsDirected α (· ≥ ·)] (a b : α) : ∃ c, c ≤ a ∧ c ≤ b :=
  directed_of (· ≥ ·) a b

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