Intersection_with_Relative_Complement_is_Empty
Provedproofwikirelative-complementset-intersection
The intersection of a set T and its relative complement in S is the empty set: T ∩ (S \ T) = ∅
Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Intersection_with_Relative_Complement_is_Empty {α : Type _} (S T : Set α) : T ∩ (S \ T) = ∅ := by sorrySource