no goals
α : Type u
β : Type ?u.20237
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y = x ↔ x \ y = x \ ⊥
rw [sdiff_bot]
no goals
α : Type u
β : Type ?u.20237
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y = x ⊓ ⊥ ↔ Disjoint y x
rw [inf_bot_eq, inf_comm, disjoint_iff]