exists_ge_ge — Mathlib

English

Let (A, ≤) be a directed poset. For any a, b ∈ A there exists c ∈ A such that a ≤ c and b ≤ c.

Русский

Пусть (A, ≤) является направленным частично упорядоченным множеством. Для любых a, b ∈ A существует c ∈ A such that a ≤ c и b ≤ c.

LaTeX

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

Lean4

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

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