α : Type u
β : Type ?u.14724
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
⊢ Disjoint z (y \ x) ↔ z ≤ x
α : Type u
β : Type ?u.14724
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
⊢ z ⊓ y \ x = ⊥ ↔ z ≤ x
rw [← disjoint_iff]
no goals
α : Type u
β : Type ?u.14724
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
⊢ Disjoint z (y \ x) ↔ z ≤ x
exact disjoint_sdiff_iff_le hz hx