ι : Type ?u.59758
α : Type u_1
β : Type ?u.59764
π : ι → Type ?u.59769
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ Disjoint ((a ⊔ b) \ (a ⊓ b)) (a ⊓ b)
ι : Type ?u.59758
α : Type u_1
β : Type ?u.59764
π : ι → Type ?u.59769
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ Disjoint (a ∆ b) (a ⊓ b)
rw [symmDiff_eq_sup_sdiff_inf]
no goals
ι : Type ?u.59758
α : Type u_1
β : Type ?u.59764
π : ι → Type ?u.59769
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ Disjoint ((a ⊔ b) \ (a ⊓ b)) (a ⊓ b)
exact disjoint_sdiff_self_left