Cartesian_Product_Distributes_over_Set_Difference
Provedcartesian-productdistributive-operationsproofwikiset-difference
Cartesian product distributes over set difference: S × (T₁ \ T₂) = (S × T₁) \ (S × T₂)
Preamble
import Mathlib.Data.Set.Prod
Formal statement
theorem Cartesian_Product_Distributes_over_Set_Difference {α : Type _} {β : Type _} (S : Set α) (T₁ T₂ : Set β) : S ×ˢ (T₁ \ T₂) = (S ×ˢ T₁) \ (S ×ˢ T₂) := by sorrySource