ι : Type ?u.66051
α : Type u_1
β : Type ?u.66057
π : ι → Type ?u.66062
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
h : a ∆ b = a ⊔ b
⊢ Disjoint a b
ι : Type ?u.66051
α : Type u_1
β : Type ?u.66057
π : ι → Type ?u.66062
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b = a ⊔ b ↔ Disjoint a b
refine' ⟨fun h => _, Disjoint.symmDiff_eq_sup⟩
ι : Type ?u.66051
α : Type u_1
β : Type ?u.66057
π : ι → Type ?u.66062
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
h : Disjoint (a ⊓ b) (a ⊔ b)
⊢ Disjoint a b
ι : Type ?u.66051
α : Type u_1
β : Type ?u.66057
π : ι → Type ?u.66062
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
h : a ∆ b = a ⊔ b
⊢ Disjoint a b
rw [symmDiff_eq_sup_sdiff_inf, sdiff_eq_self_iff_disjoint] at h
no goals
ι : Type ?u.66051
α : Type u_1
β : Type ?u.66057
π : ι → Type ?u.66062
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
h : Disjoint (a ⊓ b) (a ⊔ b)
⊢ Disjoint a b
exact h.of_disjoint_inf_of_le le_sup_left