Set_Difference_Equals_First_Set_iff_Empty_Intersection
Provedempty-setproofwikiset-differenceset-intersection
Set Difference Equals First Set iff Empty Intersection
Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Set_Difference_Equals_First_Set_iff_Empty_Intersection {α : Type _} (S T : Set α) : S \ T = S ↔ S ∩ T = ∅ := by sorry