Set_Difference_as_Intersection_with_Complement
Provedproofwikiset-complementset-differenceset-intersection
Set difference can be expressed as the intersection with the complement: A \ B = A ∩ Bᶜ
Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Set_Difference_as_Intersection_with_Complement {α : Type _} (A B : Set α) : A \ B = A ∩ Bᶜ := by sorrySource