Cartesian_Product_of_Unions

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

cartesian-productproofwikiset-union

The Cartesian product of unions: (S₁ ∪ S₂) × (T₁ ∪ T₂) = (S₁ × T₁) ∪ (S₂ × T₂) ∪ (S₁ × T₂) ∪ (S₂ × T₁)

Preamble

import Mathlib.Data.Set.Prod

Formal statement

theorem Cartesian_Product_of_Unions {α : Type _} {β : Type _} (S₁ S₂ : Set α) (T₁ T₂ : Set β) : (S₁ ∪ S₂) ×ˢ (T₁ ∪ T₂) = (S₁ ×ˢ T₁) ∪ (S₂ ×ˢ T₂) ∪ (S₁ ×ˢ T₂) ∪ (S₂ ×ˢ T₁) := by sorry

Source

https://proofwiki.org/wiki/Cartesian_Product_of_Unions

View graph