α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b x y z : α
h : IsCompl y z
⊢ x ⊓ y = ⊥ ↔ x ≤ z
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b x y z : α
h : IsCompl y z
⊢ Disjoint x y ↔ x ≤ z
rw [disjoint_iff]
no goals
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b x y z : α
h : IsCompl y z
⊢ x ⊓ y = ⊥ ↔ x ≤ z
exact h.inf_left_eq_bot_iff