description/proof of that for product map, image of product subset is product of images of component subsets under component maps
Topics
About: set
The table of contents of this article
Starting Context
- The reader knows a definition of product map.
Target Context
- The reader will have a description and a proof of the proposition that for any product map, the image of any product subset is the product of the images of the component subsets under the component maps.
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
Here is the rules of Structured Description.
Entities:
\(J\): \(\in \{\text{ the possibly uncountable index sets }\}\)
\(\{S_{1, j} \vert j \in J\}\): \(S_{1, j} \in \{\text{ the sets }\}\)
\(\{S_{2, j} \vert j \in J\}\): \(S_{2, j} \in \{\text{ the sets }\}\)
\(\{f_j \vert j \in J\}\): \(f_j: S_{1, j} \to S_{2, j}\)
\(\{S^`_{1, j} \vert j \in J\}\): \(S^`_{1, j} \subseteq S_{1, j}\)
//
Statements:
\((\times_{j \in J} f_j) (\times_{j \in J} S^`_{1, j}) = \times_{j \in J} f_j (S^`_{1, j})\)
//
2: Note
In the definition of product map, the product map by Description 1 and the product map by Description 2 are not exactly the same, but as the logics of Proof for the 2 definitions are basically the same, Proof does not distinguish them.
As a notation, for any \(s \in \times_{j \in J} S_{l, j}\), \(s^m\) denotes the \(m\)-component of \(s\).
3: Proof
Whole Strategy: Step 1: see that \((\times_{j \in J} f_j) (\times_{j \in J} S^`_{1, j}) \subseteq \times_{j \in J} f_j (S^`_{1, j})\); Step 2: see that \(\times_{j \in J} f_j (S^`_{1, j}) \subseteq (\times_{j \in J} f_j) (\times_{j \in J} S^`_{1, j})\); Step 3: conclude the proposition.
Step 1:
Let \(s \in (\times_{j \in J} f_j) (\times_{j \in J} S^`_{1, j})\) be any.
There is an \(s' \in \times_{j \in J} S^`_{1, j}\) such that \(s = (\times_{j \in J} f_j) (s')\).
\(s' \in \times_{j \in J} S^`_{1, j}\) means that \(s'^j \in S^`_{1, j}\), so, \(f_j (s'^j) \in f_j (S^`_{1, j})\).
\(s = (\times_{j \in J} f_j) (s') = \times_{j \in J} f_j (s'^j) \subseteq \times_{j \in J} f_j (S^`_{1, j})\).
So, \((\times_{j \in J} f_j) (\times_{j \in J} S^`_{1, j}) \subseteq \times_{j \in J} f_j (S^`_{1, j})\).
Step 2:
Let \(s \in \times_{j \in J} f_j (S^`_{1, j})\) be any.
\(s^j \in f_j (S^`_{1, j})\).
There is an \(s'^j \in S^`_{1, j}\) such that \(s^j = f_j (s'^j)\).
\(\times_{j \in J} s'^j \in \times_{j \in J} S^`_{1, j}\).
\(s = \times_{j \in J} s^j = (\times_{j \in J} f_j) (\times_{j \in J} s'^j) \in (\times_{j \in J} f_j) (\times_{j \in J} S^`_{1, j})\).
So, \(\times_{j \in J} f_j (S^`_{1, j}) \subseteq (\times_{j \in J} f_j) (\times_{j \in J} S^`_{1, j})\).
Step 3:
So, \((\times_{j \in J} f_j) (\times_{j \in J} S^`_{1, j}) = \times_{j \in J} f_j (S^`_{1, j})\).
