description/proof of that for product set, product subset one of whose components is subtraction of \(2\) subsets is subtraction of product subsets whose corresponding components are 1st subset and 2nd subset
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 subtraction of any \(2\) subsets is the subtraction of the product subsets whose corresponding components are the 1st subset and the 2nd subset.
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 }\} \vert j \in J\}\):
\(S_{l, 1}\): \(\subseteq S_l\)
\(S_{l, 2}\): \(\subseteq S_l\)
\(\{S'_j \in \{\text{ the sets }\} \vert j \in J \land (\forall j \in J \setminus \{l\} (S'_j = S_j); S'_l = S_{l, 1} \setminus S_{l, 2})\}\):
\(\{S''_j \in \{\text{ the sets }\} \vert j \in J \land (\forall j \in J \setminus \{l\} (S''_j = S_j); S''_l = S_{l, 1})\}\):
\(\{S'''_j \in \{\text{ the sets }\} \vert j \in J \land (\forall j \in J \setminus \{l\} (S'''_j = S_j); S'''_l = S_{l, 2})\}\):
\(\times_{j \in J} S'_j\):
\(\times_{j \in J} S''_j\):
\(\times_{j \in J} S'''_j\):
//
Statements:
\(\times_{j \in J} S'_j = \times_{j \in J} S''_j \setminus \times_{j \in J} S'''_j\)
//
2: Proof 1
Whole Strategy: Step 1: see that \(\times_{j \in J} S'_j \subseteq \times_{j \in J} S''_j \setminus \times_{j \in J} S'''_j\); Step 2: see that \(\times_{j \in J} S''_j \setminus \times_{j \in J} S'''_j \subseteq \times_{j \in J} S'_j\); Step 3: conclude the proposition.
Step 1:
Let \(f \in \times_{j \in J} S'_j\) be any.
For each \(j \in J\), \(f (j) \in S'_j\).
For each \(j \in J \setminus \{l\}\), \(f (j) \in S'_j = S''_j\).
\(f (l) \in S'_l = S_{l, 1} \setminus S_{l, 2} \subseteq S_{l, 1} = S''_l\).
So, \(f \in \times_{j \in J} S''_j\).
\(f (l) \in S_{l, 1} \setminus S_{l, 2}\), which means that \(f (l) \notin S_{l, 2} = S'''_l\), which means that \(f \notin \times_{j \in J} S'''_j\).
So, \(f \in \times_{j \in J} S''_j \setminus \times_{j \in J} S'''_j\).
Step 2:
Let \(f \in \times_{j \in J} S''_j \setminus \times_{j \in J} S'''_j\) be any.
\(f \in \times_{j \in J} S''_j\) and \(f \notin \times_{j \in J} S'''_j\).
For each \(j \in J\), \(f (j) \in S''_j\).
For each \(j \in J \setminus \{l\}\), \(f (j) \in S''_j = S'''_j = S'_j\), so, \(f \notin \times_{j \in J} S'''_j\) means that \(f (l) \notin S'''_l\), so, \(f (l) \in S''_l \setminus S'''_l = S_{l, 1} \setminus S_{l, 2} = S'_l\).
So, \(f \in \times_{j \in J} S'_j\).
Step 3:
So, \(\times_{j \in J} S'_j = \times_{j \in J} S''_j \setminus \times_{j \in J} S'''_j\).
3: Structured Description 2
Here is the rules of Structured Description.
Entities:
\(\{S_1, ..., S_n\}\): \(S_j \in \{\text{ the sets }\}\)
\(S_{l, 1}\): \(\subseteq S_l\)
\(S_{l, 2}\): \(\subseteq S_l\)
\(\{S'_1, ..., S'_n\}\): \(\forall j \in J \setminus \{l\} (S'_j = S_j); S'_l = S_{l, 1} \setminus S_{l, 2}\)
\(\{S''_1, ..., S''_n\}\): \(\forall j \in J \setminus \{l\} (S''_j = S_j); S''_l = S_{l, 1}\)
\(\{S'''_1, ..., S'''_n\}\): \(\forall j \in J \setminus \{l\} (S'''_j = S_j); S'''_l = S_{l, 2}\)
\(S'_1 \times ... \times S'_n\):
\(S''_1 \times ... \times S''_n\):
\(S'''_1 \times ... \times S'''_n\):
//
Statements:
\(S'_1 \times ... \times S'_n = (S''_1 \times ... \times S''_n) \setminus (S'''_1 \times ... \times S'''_n)\)
//
4: Proof 2
Whole Strategy: Step 1: see that \(S'_1 \times ... \times S'_n \subseteq (S''_1 \times ... \times S''_n) \setminus (S'''_1 \times ... \times S'''_n)\); Step 2: see that \((S''_1 \times ... \times S''_n) \setminus (S'''_1 \times ... \times S'''_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\}\), \(p^j \in S'_j = S''_j\).
\(p^l \in S'_l = S_{l, 1} \setminus S_{l, 2} \subseteq S_{l, 1} = S''_l\).
So, \(p \in S''_1 \times ... \times S''_n\).
\(p^l \in S_{l, 1} \setminus S_{l, 2}\), which means that \(p^l \notin S_{l, 2} = S'''_l\), which means that \(p \notin S'''_1 \times ... \times S'''_n\).
So, \(p \in (S''_1 \times ... \times S''_n) \setminus (S'''_1 \times ... \times S'''_n)\).
Step 2:
Let \(p = (p^1, ..., p^n) \in (S''_1 \times ... \times S''_n) \setminus (S'''_1 \times ... \times S'''_n)\) be any.
\(p \in S''_1 \times ... \times S''_n\) and \(p \notin S'''_1 \times ... \times S'''_n\).
For each \(j \in \{1, ..., n\}\), \(p^j \in S''_j\).
For each \(j \in \{1, ..., n\} \setminus \{l\}\), \(p^j \in S''_j = S'''_j = S'_j\), so, \(p \notin S'''_1 \times ... \times S'''_n\) means that \(p^l \notin S'''_l\), so, \(p^l \in S''_l \setminus S'''_l = S_{l, 1} \setminus S_{l, 2} = S'_l\).
So, \(f \in S'_1 \times ... \times S'_n\).
Step 3:
So, \(S'_1 \times ... \times S'_n = (S''_1 \times ... \times S''_n) \setminus (S'''_1 \times ... \times S'''_n)\).
