English
Dual to disjointness, in a SemilatticeSup context, x ⊔ y reaches the top b iff Codisjoint x y holds, i.e., x.1 ⊔ y.1 = b.
Русский
Дубль для сопряженного случая: Codisjoint x y эквивалентно тому, что верхний предел достигает b, то есть x.1 ⊔ y.1 = b.
LaTeX
$$$\text{Codisjoint}(x,y) \iff x^{\uparrow} \! \lor y^{\uparrow} = b$$$
Lean4
protected theorem codisjoint_iff [SemilatticeSup α] [Fact (a ≤ b)] {x y : Icc a b} :
Codisjoint x y ↔ ↑x ⊔ (y : α) = b := by simp [_root_.codisjoint_iff, Subtype.ext_iff]