description/proof of that for product set, product subset one of whose components is union of subsets is union of product subsets whose corresponding components are subsets
Topics
About: set
The table of contents of this article
- Starting Context
- Target Context
- Orientation
- Main Body
- 1: Structured Description 1
- 2: Proof 1
- 3: Structured Description 2
- 4: Proof 2
Starting Context
- The reader knows a definition of product set.
Target Context
- The reader will have a description and a proof of the proposition that for any product set, any product subset one of whose components is the union of any subsets is the union of the product subsets whose corresponding components are the subsets.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description 1
Here is the rules of Structured Description.
Entities:
\(J_1\): \(\in \{\text{ the possibly uncountable index sets }\}\)
\(J_2\): \(\in \{\text{ the possibly uncountable index sets }\}\)
\(\{S_j \in \{\text{ the sets }\} \vert j \in J_1 \setminus \{l\}\}\):
\(\{S_{l, m} \in \{\text{ the sets }\} \vert m \in J_2\}\):
\(\{S'_j \in \{\text{ the sets }\} \vert j \in J_1 \land (\forall j \in J_1 \setminus \{l\} (S'_j = S_j); S'_l = \cup_{m \in J_2} S_{l, m})\}\):
\(\{S'_{m, j} \in \{\text{ the sets }\} \vert m \in J_2, j \in J_1 \land (\forall j \in J_1 \setminus \{l\} (S'_{m, j} = S_j); S'_{m, l} = S_{l, m})\}\):
\(\times_{j \in J_1} S'_j\):
\(\cup_{m \in J_2} \times_{j \in J_1} S'_{m, j}\):
//
Statements:
\(\times_{j \in J_1} S'_j = \cup_{m \in J_2} \times_{j \in J_1} S'_{m, j}\)
//
2: Proof 1
Whole Strategy: Step 1: see that \(\times_{j \in J_1} S'_j \subseteq \cup_{m \in J_2} \times_{j \in J_1} S'_{m, j}\); Step 2: see that \(\cup_{m \in J_2} \times_{j \in J_1} S'_{m, j} \subseteq \times_{j \in J_1} S'_j\); Step 3: conclude the proposition.
Step 1:
Let \(f \in \times_{j \in J_1} S'_j\) be any.
For each \(j \in J_1\), \(f (j) \in S'_j\).
For each \(j \in J_1 \setminus \{l\}\), \(S'_j = S'_{m, j}\) for each \(m \in J_2\).
\(f (l) \in S'_l = \cup_{m \in J_2} S_{l, m}\).
So, \(f (l) \in S_{l, m} = S'_{m, l}\) for an \(m \in J_2\).
So, for that \(m\), \(f \in \times_{j \in J_1} S'_{m, j}\).
So, \(f \in \cup_{m \in J_2} \times_{j \in J_1} S'_{m, j}\).
Step 2:
Let \(f \in \cup_{m \in J_2} \times_{j \in J_1} S'_{m, j}\) be any.
\(f \in \times_{j \in J_1} S'_{m, j}\) for an \(m \in J_2\).
For that \(m\), for each \(j \in J_1\), \(f (j) \in S'_{m, j}\), but for each \(j \in J_1 \setminus \{l\}\), \(S'_{m, j} = S_j = S'_j\), and \(S'_{m, l} = S_{l, m} \subseteq \cup_{m' \in J_2} S_{l, m'} = S'_l\).
So, \(f \in \times_{j \in J_1} S'_j\).
Step 3:
So, \(\times_{j \in J_1} S'_j = \cup_{m \in J_2} \times_{j \in J_1} S'_{m, j}\).
3: Structured Description 2
Here is the rules of Structured Description.
Entities:
\(J_2\): \(\in \{\text{ the possibly uncountable index sets }\}\)
\(\{S_1, ..., S_{l - 1}, \widehat{S_l}, S_{l + 1}, ..., S_n\}\): \(S_j \in \{\text{ the sets }\}\)
\(\{S_{l, m} \in \{\text{ the sets }\} \vert m \in J_2\}\):
\(\{S'_1, ..., S'_n\}\): \(\forall j \in \{1, ..., n\} \setminus \{l\} (S'_j = S_j); S'_l = \cup_{m \in J_2} S_{l, m}\)
\(\{S'_{m, 1}, ..., S'_{m, n} \vert m \in J_2\}\): \(\forall j \in \{1, ..., n\} \setminus \{l\} (S'_{m, j} = S_j); S'_{m, l} = S_{l, m}\)
\(S'_1 \times ... \times S'_n\):
\(\cup_{m \in J_2} S'_{m, 1} \times ... \times S'_{m, n}\):
//
Statements:
\(S'_1 \times ... \times S'_n = \cup_{m \in J_2} S'_{m, 1} \times ... \times S'_{m, n}\)
//
4: Proof 2
Whole Strategy: Step 1: see that \(S'_1 \times ... \times S'_n \subseteq \cup_{m \in J_2} S'_{m, 1} \times ... \times S'_{m, n}\); Step 2: see that \(\cup_{m \in J_2} S'_{m, 1} \times ... \times S'_{m, n} \subseteq S'_1 \times ... \times S'_n\); Step 3: conclude the proposition.
Step 1:
Let \(p = (p^1, ..., p^n) \in S'_1 \times ... \times S'_n\) be any.
For each \(j \in \{1, ..., n\}\), \(p^j \in S'_j\).
For each \(j \in \{1, ..., n\} \setminus \{l\}\), \(S'_j = S'_{m, j}\) for each \(m \in J_2\).
\(p^l \in S'_l = \cup_{m \in J_2} S_{l, m}\).
So, \(p^l \in S_{l, m} = S'_{m, l}\) for a \(m \in J_2\).
So, for that \(m\), \(p \in S'_{m, 1} \times ... \times S'_{m, n}\).
So, \(p \in \cup_{m \in J_2} S'_{m, 1} \times ... \times S'_{m, n}\).
Step 2:
Let \(p \in \cup_{m \in J_2} S'_{m, 1} \times ... \times S'_{m, n}\) be any.
\(p \in S'_{m, 1} \times ... \times S'_{m, n}\) for an \(m \in J_2\).
For that \(m\), for each \(j \in \{1, ..., n\}\), \(p^j \in S'_{m, j}\), but for each \(j \in \{1, ..., n\} \setminus \{l\}\), \(S'_{m, j} = S_j = S'_j\), and \(S'_{m, l} = S_{l, m} \subseteq \cup_{m' \in J_2} S_{l, m'} = S'_l\).
So, \(p \in S'_1 \times ... \times S'_n\).
Step 3:
So, \(S'_1 \times ... \times S'_n = \cup_{m \in J_2} S'_{m, 1} \times ... \times S'_{m, n}\).
