codisjoint_iff — Mathlib

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]

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