ThmDex – An index of mathematical definitions, results, and conjectures.
Set of symbols
Alphabet
Deduction system
Theory
Zermelo-Fraenkel set theory
Set
Binary cartesian set product
Binary relation
Map
Definition D326
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}
Children
D327: Canonical set projection
D5639: Complex cartesian product
D2758: Cylinder set
D68: Set of maps
Results
R4630: Bijection between parenthesis-sliced cartesian triple products
R4315: Cardinality of a finite set raised to a finite power
R4632: Cardinality of cartesian triple products is invariant under insertion of parentheses
R4631: Cardinality of finite cartesian products is invariant under insertion of parentheses
R221: Cartesian product is not associative
R4263: Countable cartesian product with empty set is empty
R4262: Finite cartesian product with empty set is empty