Empty_Set_is_Unique
Provedempty-setempty-set-is-uniqueproofwiki
The empty set is unique.
Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Empty_Set_is_Unique {α : Type*} (S T : Set α) (hS : S = ∅) (hT : T = ∅) : S = T := by sorrySource