Set of symbols
Alphabet
Deduction system
Theory
Zermelo-Fraenkel set theory
Set
Binary cartesian set product
Binary relation
Map
Cartesian product
Formulation 0
Let $X_j$ be a D11: Set for each $j \in J$ such that
(i) $\bigcup_{j \in J} X_j$ is the D77: Set union of $X = \{ X_j \}_{j \in J}$
The cartesian product of $X = \{ X_j \}_{j \in J}$ is the D11: Set \begin{equation} \prod_{j \in J} X_j : = \left\{ x : J \to \bigcup_{j \in J} X_j \mid \forall \, j \in J : x_j \in X_j \right\} \end{equation}
Dual definition
» Disjoint union
Also known as
Set direct product
Child definitions
» D327: Canonical set projection
» D5639: Complex cartesian product
» D2758: Cylinder set
» D68: Set of maps
Results
» R1832: Cardinality of a finite cartesian product of finite sets
» R4263: Countable cartesian product with empty set is empty
» R4264: Cartesian product with empty set is empty
» R221: Cartesian product is not associative
» R4060: Appropriately parenthesised cartesian products are isomorphic
» R4262: Finite cartesian product with empty set is empty
» R4315: Cardinality of a finite set raised to a finite power
» R4631: Cardinality of finite cartesian products is invariant under insertion of parentheses
» R1848: Bijection between parenthesis-sliced cartesian products
» R4630: Bijection between parenthesis-sliced cartesian triple products
» R4632: Cardinality of cartesian triple products is invariant under insertion of parentheses
» R4887: Cardinality of binary cartesian product of finite sets