Cartesian_Product_is_Empty_iff_Factor_is_Empty
Provedcartesian-productempty-setproofwiki
The Cartesian product S × T is empty if and only if S is empty or T is empty.
Preamble
import Mathlib.Data.Set.Prod
Formal statement
theorem Cartesian_Product_is_Empty_iff_Factor_is_Empty {α : Type _} {β : Type _} (S : Set α) (T : Set β) : S ×ˢ T = ∅ ↔ S = ∅ ∨ T = ∅ := by sorrySource