Set_Difference_of_Cartesian_Products
Provedcartesian-productproofwikiset-difference
The set difference of Cartesian products: (S₁ × S₂) \ (T₁ × T₂) = (S₁ × (S₂ \ T₂)) ∪ ((S₁ \ T₁) × S₂)
Preamble
import Mathlib.Data.Set.Prod
Formal statement
theorem Set_Difference_of_Cartesian_Products {α : Type _} {β : Type _} (S₁ : Set α) (S₂ : Set β) (T₁ : Set α) (T₂ : Set β) : (S₁ ×ˢ S₂) \ (T₁ ×ˢ T₂) = (S₁ ×ˢ (S₂ \ T₂)) ∪ ((S₁ \ T₁) ×ˢ S₂) := by sorrySource