Cartesian_Product_is_Anticommutative
Provedcartesian-productproofwiki
Let S, T be nonempty sets. Then S × T = T × S implies S = T.
Preamble
import Mathlib.Data.Set.Prod
Formal statement
theorem Cartesian_Product_is_Anticommutative {α : Type _} (S T : Set α) (hS : S.Nonempty) (hT : T.Nonempty) (h : S ×ˢ T = T ×ˢ S) : S = T := by sorrySource