Union_is_Empty_iff_Sets_are_Empty
Provedempty-setproofwikiset-union
S ∪ T = ∅ if and only if S = ∅ and T = ∅.
Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Union_is_Empty_iff_Sets_are_Empty {α : Type _} (S T : Set α) : S ∪ T = ∅ ↔ S = ∅ ∧ T = ∅ := by sorrySource