ι : Type ?u.66703
α : Type u_1
β : Type ?u.66709
π : ι → Type ?u.66714
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
h : a ≤ a ∆ b
⊢ Disjoint a b
ι : Type ?u.66703
α : Type u_1
β : Type ?u.66709
π : ι → Type ?u.66714
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ≤ a ∆ b ↔ Disjoint a b
refine' ⟨fun h => _, fun h => h.symmDiff_eq_sup.symm ▸ le_sup_left⟩
ι : Type ?u.66703
α : Type u_1
β : Type ?u.66709
π : ι → Type ?u.66714
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
h : a ≤ (a ⊔ b) \ (a ⊓ b)
⊢ Disjoint a b
ι : Type ?u.66703
α : Type u_1
β : Type ?u.66709
π : ι → Type ?u.66714
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
h : a ≤ a ∆ b
⊢ Disjoint a b
rw [symmDiff_eq_sup_sdiff_inf] at h
no goals
ι : Type ?u.66703
α : Type u_1
β : Type ?u.66709
π : ι → Type ?u.66714
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
h : a ≤ (a ⊔ b) \ (a ⊓ b)
⊢ Disjoint a b
exact disjoint_iff_inf_le.mpr (le_sdiff_iff.1 <| inf_le_of_left_le h).le