ThmDex – An index of mathematical definitions, results, and conjectures.
Set of symbols
Alphabet
Deduction system
Theory
Zermelo-Fraenkel set theory
Set
Collection of sets
Definition D77
Set union
Formulation 0
Let $E_j$ be a D11: Set for every $j \in J$.
The union of $E = \{ E_j \}_{j \in J}$ is the D11: Set \begin{equation} \bigcup_{j \in J} E_j : = \{ x \mid \exists \, j \in J : x \in E_j \} \end{equation}
Formulation 1
Let $x$ be a D11: Set.
The union of $x$ is the D11: Set \begin{equation} \cup x : = \{ z \mid \exists \, y \in x : z \in y \} \end{equation}
Children
Disjoint union
Set cover
Successor set
Results
Binary set union is commutative
Binary union is an upper bound to both sets in the union
Countable set union is invariant under bijective shifting of indices
Countable union is an upper bound to each set in the union
Finite set union is invariant under bijective shifting of indices
Finite union is an upper bound to each set in the union
Isotonicity of set union
Superset of binary union iff superset of both sets in the union
Superset of countable union iff superset of every set in the union
Superset of finite union iff superset of every set in the union
Union is smallest upper bound
Union is upper bound for intersection