Set_Difference_with_Empty_Set_is_Self
Provedempty-setproofwikiset-difference
Set Difference with Empty Set is Self
Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Set_Difference_with_Empty_Set_is_Self {α : Type _} (S : Set α) : S \ ∅ = S := by sorry