English
Two elements a and b are codisjoint if, whenever a ≤ x and b ≤ x for some x, then x must be the top element.
Русский
Два элемента a и b называются кодиссоединёнными, если для любого x, удовлетворяющего a ≤ x и b ≤ x, выполняется ⊤ ≤ x.
LaTeX
$$$\operatorname{Codisjoint}(a,b) := \forall x, a \le x \to b \le x \to \top \le x$$$
Lean4
/-- Two elements of a lattice are codisjoint if their sup is the top element.
Note that we define this without reference to `⊔`, as this allows us to talk about orders where
the supremum is not unique, or where implement `Sup` would require additional `Decidable`
arguments. -/
def Codisjoint (a b : α) : Prop :=
∀ ⦃x⦄, a ≤ x → b ≤ x → ⊤ ≤ x
