description/proof of that product subset of product set is intersection of product subsets each of which takes component subset and other whole sets
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 set.
Target Context
- The reader will have a description and a proof of the proposition that any product subset of any product set is the intersection of the product subsets each of which takes a component subset and the other whole sets.
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\): \(\in \{\text{ the possibly uncountable index sets }\}\)
\(\{S'_j \in \{\text{ the sets }\}: j \in J\}\):
\(\times_{j \in J} S'_j\):
\(\{S_j \subseteq S'_j: j \in J\}\):
\(\times_{j \in J} S_j\): \(\subseteq \times_{j \in J} S'_j\)
//
Statements:
\(\times_{j \in J} S_j = \cap_{l \in J} \times_{j \in J} S_{l, j}\) where \(S_{l, j} = S_l\) when \(j = l\) and \(S_{l, j} = S'_j\) otherwise
//
\(\times_{j \in J} S_j\) is regarded to be a subset of \(\times_{j \in J} S'_j\), because for each \(p \in \times_{j \in J} S_j\), \(p\) is a function from \(J\) into \(\cup_{j \in J} S_j\) such that \(p (j) \in S_j\), which is regarded to be a function from \(J\) into \(\cup_{j \in J} S'_j\) such that \(p (j) \in S'_j\).
2: Proof 1
Whole Strategy: Step 1: for each \(p \in \times_{j \in J} S_j\), see that \(p \in \cap_{l \in J} \times_{j \in J} S_{l, j}\); Step 2: for each \(p \in \cap_{l \in J} \times_{j \in J} S_{l, j}\), see that \(p \in \times_{j \in J} S_j\).
Step 1:
Let \(p \in \times_{j \in J} S_j\) be any.
For each \(l \in J\), \(p \in \times_{j \in J} S_{l, j}\), because for \(j = l\), \(p (j) \in S_l = S_{l, j}\), and for each \(j \neq l\), \(p (j) \in S'_j = S_{l, j}\).
So, \(p \in \cap_{l \in J} \times_{j \in J} S_{l, j}\).
Step 2:
Let \(p \in \cap_{l \in J} \times_{j \in J} S_{l, j}\) be any.
For each \(l \in J\), \(p \in \times_{j \in J} S_{l, j}\), for each \(j \in J\), \(p (j) \in S_{l, j}\), so, \(p (l) \in S_{l, l} = S_l\).
So, \(p \in \times_{j \in J} S_j\).
3: Structured Description 2
Here is the rules of Structured Description.
Entities:
\(\{S'_1, ..., S'_n\}\):
\(S'_1 \times ... \times S'_n\):
\(\{S_1 \subseteq S'_1, ..., S_n \subseteq S'_n\}\):
\(S_1 \times ... \times S_n\): \(\subseteq S'_1 \times ... \times S'_n\)
//
Statements:
\(S_1 \times ... \times S_n = \cap_{l \in \{1, ..., n\}} S_{l, 1} \times ... \times S_{l, n}\) where \(S_{l, j} = S_l\) when \(j = l\) and \(S_{l, j} = S'_j\) otherwise
//
4: Proof 2
Whole Strategy: Step 1: for each \(p \in S_1 \times ... \times S_n\), see that \(p \in \cap_{l \in \{1, ..., n\}} S_{l, 1} \times ... \times S_{l, n}\); Step 2: for each \(p \in \cap_{l \in \{1, ..., n\}} S_{l, 1} \times ... \times S_{l, n}\), see that \(p \in S_1 \times ... \times S_n\).
Step 1:
Let \(p = (p_1, ..., p_n) \in S_1 \times ... \times S_n\) be any.
For each \(l \in \{1, ..., n\}\), \(p \in S_{l, 1} \times ... \times S_{l, n}\), because \(p_j \in S_l = S_{l, j}\) for \(j = l\) and \(p_j \in S'_j = S_{l, j}\) otherwise.
So, \(p \in \cap_{l \in \{1, ..., n\}} S_{l, 1} \times ... \times S_{l, n}\).
Step 2:
Let \(p = (p_1, ..., p_n) \in \cap_{l \in \{1, ..., n\}} S_{l, 1} \times ... \times S_{l, n}\) be any.
For each \(l \in \{1, ..., n\}\), \(p \in S_{l, 1} \times ... \times S_{l, n}\), so, \(p_l \in S_{l, l} = S_l\).
So, \(p \in S_1 \times ... \times S_n\).
