Empty_Set_is_Unique_v2
Provedproofwikiretry
The empty set is unique.
Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Empty_Set_is_Unique_v2 {α : Type _} (S T : Set α) (hS : S = ∅) (hT : T = ∅) : S = T := by sorryThe empty set is unique.
import Mathlib.Data.Set.Basic
theorem Empty_Set_is_Unique_v2 {α : Type _} (S T : Set α) (hS : S = ∅) (hT : T = ∅) : S = T := by sorry