description/proof of that for map and its extension that maps extended area outside original codomain, original map image of subset of original domain is intersection of extension image of union of subset and extended area and original codomain
Topics
About: set
The table of contents of this article
Starting Context
- The reader knows a definition of map preimage of subset of codomain.
Target Context
- The reader will have a description and a proof of the proposition that for any map and its any extension that maps the extended area outside the original codomain, the original map image of any subset of the original domain is the intersection of the extension image of the union of the subset and the extended area and the original codomain.
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:
\(S'_1\): \(\in \{\text{ the sets }\}\)
\(S'_2\): \(\in \{\text{ the sets }\}\)
\(S_1\): \(\subseteq S'_1\)
\(S_2\): \(\subseteq S'_2\)
\(f\): \(: S_1 \to S_2\)
\(f'\): \(: S'_1 \to S'_2\), such that \(f' (S'_1 \setminus S_1) \subseteq S'_2 \setminus S_2\)
\(S\): \(\subseteq S_1\)
//
Statements:
\(f (S) = f' (S \cup (S'_1 \setminus S_1)) \cap S_2\)
//
2: Proof
Whole Strategy: Step 1: see that \(f (S) \subseteq f' (S \cup (S'_1 \setminus S_1)) \cap S_2\); Step 2: see that \(f' (S \cup (S'_1 \setminus S_1)) \cap S_2 \subseteq f (S)\); Step 3: conclude the proposition.
Step 1:
For each \(p \in f (S)\), \(p = f (s)\) for an \(s \in S\), \(p = f (s) = f' (s) \in f' (S \cup (S'_1 \setminus S_1)) \cap S_2\).
So, \(f (S) \subseteq f' (S \cup (S'_1 \setminus S_1)) \cap S_2\).
Step 2:
For each \(p \in f' (S \cup (S'_1 \setminus S_1)) \cap S_2\), \(p = f' (s)\) for an \(s \in S \cap S_1\), because \(f' (S'_1 \setminus S_1) \subseteq S'_2 \setminus S_2\), so, \(p = f' (s) = f (s)\) where \(s \in S \cap S_1 \subseteq S\), so, \(p \in f (S)\).
So, \(f' (S \cup (S'_1 \setminus S_1)) \cap S_2 \subseteq f (S)\).
Step 3:
So, \(f (S) = f' (S \cup (S'_1 \setminus S_1)) \cap S_2\).
