Set_Difference_as_Intersection_with_Relative_Complement
Provedproofwikirelative-complementset-differenceset-intersection
Let A, B ⊆ S. Then the set difference A \ B equals the intersection A ∩ (S \ B).
Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Set_Difference_as_Intersection_with_Relative_Complement {α : Type _} (S A B : Set α) (hA : A ⊆ S) (hB : B ⊆ S) : A \ B = A ∩ (S \ B) := by sorrySource