Cartesian_Product_of_Intersections
Provedcartesian-productproofwikiset-intersection
The Cartesian product of intersections equals the intersection of Cartesian products: (S₁ ∩ S₂) × (T₁ ∩ T₂) = (S₁ × T₁) ∩ (S₂ × T₂)
Preamble
import Mathlib.Data.Set.Prod
Formal statement
theorem Cartesian_Product_of_Intersections {α : Type _} {β : Type _} (S₁ S₂ : Set α) (T₁ T₂ : Set β) : (S₁ ∩ S₂) ×ˢ (T₁ ∩ T₂) = (S₁ ×ˢ T₁) ∩ (S₂ ×ˢ T₂) := by sorrySource