description/proof of that for product set, product of intersections of subsets of constituent sets is intersection of products of subsets
Topics
About: set
The table of contents of this article
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 and any set of subsets of each constituent set, the product of the intersections of the subsets of the constituent sets is the intersection of the products of 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
Here is the rules of Structured Description.
Entities:
\(J\): \(\in \{\text{ the possibly uncountable index sets }\}\)
\(\{S_j \in \{\text{ the sets }\} \vert j \in J\}\):
\(\times_{j \in J} S_j\): \(= \text{ the product set }\)
\(\{L_j \in \{\text{ the possibly uncountable index sets }\} \vert j \in J\}\):
\(\{S_{j, l_j} \subseteq S_j \vert j \in J, l_j \in L_j\}\):
\(\times_{j \in J} L_j\): \(= \text{ the product set }\)
//
Statements:
\(\times_{j \in J} \cap_{l_j \in L_j} S_{j, l_j} = \cap_{f \in \times_{j \in J} L_j} \times_{j \in J} S_{j, f (j)}\)
//
2: Proof
Whole Strategy: Step 1: see that \(\times_{j \in J} \cap_{l_j \in L_j} S_{j, l_j} \subseteq \cap_{f \in \times_{j \in J} L_j} \times_{j \in J} S_{j, f (j)}\); Step 2: see that \(\cap_{f \in \times_{j \in J} L_j} \times_{j \in J} S_{j, f (j)} \subseteq \times_{j \in J} \cap_{l_j \in L_j} S_{j, l_j}\); Step 3: conclude the proposition.
Step 0:
For any product set, \(\times_{j \in J} S_j\), and any \(s \in \times_{j \in J} S_j\), let \(s^j = s (j)\) denote the \(j\)-component of the element.
Step 1:
Let \(s \in \times_{j \in J} \cap_{l_j \in L_j} S_{j, l_j}\) be any.
For each \(j \in J\), \(s^j \in \cap_{l_j \in L_j} S_{j, l_j}\), so, \(s^j \in S_{j, l_j}\) for each \(l_j \in L_j\).
For each \(f \in \times_{j \in J} L_j\), \(f (j) \in L_j\) for each \(j \in J\), so, \(s^j \in S_{j, f (j)}\) for each \(j \in J\).
\(s \in \times_{j \in J} S_{j, f (j)}\).
So, \(s \in \cap_{f \in \times_{j \in J} L_j} \times_{j \in J} S_{j, f (j)}\).
So, \(\times_{j \in J} \cap_{l_j \in L_j} S_{j, l_j} \subseteq \cap_{f \in \times_{j \in J} L_j} \times_{j \in J} S_{j, f (j)}\).
Step 2:
Let \(s \in \cap_{f \in \times_{j \in J} L_j} \times_{j \in J} S_{j, f (j)}\) be any.
\(s \in \times_{j \in J} S_{j, f (j)}\) for each \(f \in \times_{j \in J} L_j\).
For each \(j \in J\), \(s^j \in S_{j, f (j)}\).
As for each \(l_j \in L_j\), there is an \(f \in \times_{j \in J} L_j\) such that \(f (j) = l_j\), \(s^j \in S_{j, l_j}\) for each \(l_j \in L_j\), so, \(s^j \in \cap_{l_j \in L_j} S_{j, l_j}\).
So, \(s \in \times_{j \in J} \cap_{l_j \in L_j} S_{j, l_j}\).
So, \(\cap_{f \in \times_{j \in J} L_j} \times_{j \in J} S_{j, f (j)} \subseteq \times_{j \in J} \cap_{l_j \in L_j} S_{j, l_j}\).
Step 3:
So, \(\times_{j \in J} \cap_{l_j \in L_j} S_{j, l_j} = \cap_{f \in \times_{j \in J} L_j} \times_{j \in J} S_{j, f (j)}\).
