ι : Type ?u.76942
α : Type u_1
β : Type ?u.76948
π : ι → Type ?u.76953
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
ha : Disjoint a c
hb : Disjoint b c
⊢ Disjoint ((a ⊔ b) \ (a ⊓ b)) c
ι : Type ?u.76942
α : Type u_1
β : Type ?u.76948
π : ι → Type ?u.76953
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
ha : Disjoint a c
hb : Disjoint b c
⊢ Disjoint (a ∆ b) c
rw [symmDiff_eq_sup_sdiff_inf]
no goals
ι : Type ?u.76942
α : Type u_1
β : Type ?u.76948
π : ι → Type ?u.76953
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
ha : Disjoint a c
hb : Disjoint b c
⊢ Disjoint ((a ⊔ b) \ (a ⊓ b)) c
exact (ha.sup_left hb).disjoint_sdiff_left