description/proof of that for map, subset of domain, and point of codomain, if intersection of preimage of point and subset is preimage, preimage of point is contained in subset or is disjoint from subset
Topics
About: set
The table of contents of this article
Starting Context
- The reader knows a definition of map preimage of subset of codomain.
- The reader admits the proposition that the preimages of any disjoint subsets under any map are disjoint.
Target Context
- The reader will have a description and a proof of the proposition that for any map, any subset of the domain, and any point of the codomain, if the intersection of the preimage of the point and the subset is a preimage, the preimage of the point is contained in the subset or is disjoint from the 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
Here is the rules of Structured Description.
Entities:
\(S'_1\): \(\in \{\text{ the sets }\}\)
\(S'_2\): \(\in \{\text{ the sets }\}\)
\(f\): \(: S'_1 \to S'_2\)
\(S_1\): \(\subseteq S'_1\)
\(s'_2\): \(\in S'_2\)
//
Statements:
\(\exists S_2 \subseteq S'_2 (f^{-1} (s'_2) \cap S_1 = f^{-1} (S_2))\)
\(\implies\)
\(f^{-1} (s'_2) \subseteq S_1 \lor f^{-1} (s'_2) \cap S_1 = \emptyset\)
//
2: Note
\(s'_2\) cannot be replaced by a subset, \({S'_2}^` \subseteq S'_2\), for this proposition: for each \(s'_2 \in {S'_2}^`\), this proposition holds, but for some \(s'_2, \widetilde{s'_2} \in {S'_2}^`\) such that \(s'_2 \neq \widetilde{s'_2}\), it may be that \(f^{-1} (s'_2) \subseteq S_1\) and \(f^{-1} (\widetilde{s'_2}) \cap S_1 = \emptyset\), for example, then, \(f^{-1} ({S'_2}^`) \subseteq S_1 \lor f^{-1} ({S'_2}^`) \cap S_1 = \emptyset\) does not hold.
For example, let \(f: \{0, 1\} \to \{0, 1\} = id\), \(S_1 = \{1\}\), and \(S_2 = \{0, 1\}\), then, \(f^{-1} (\{0, 1\}) = \{0, 1\}\) and \(f^{-1} (\{0, 1\}) \cap \{1\} = \{1\} = f^{-1} (\{1\})\), but not \(\{0, 1\} \subseteq \{1\}\) nor \(\{0, 1\} \cap \{1\} = \emptyset\) holds: for \(s'_2 = 0\), \(f^{-1} (0) = \{0\}\) and \(f^{-1} (0) \cap \{1\} = \emptyset = f^{-1} (\emptyset)\), and \(f^{-1} (0) \cap \{1\} = \emptyset\) holds; for \(s'_2 = 1\), \(f^{-1} (1) = \{1\}\) and \(f^{-1} (1) \cap \{1\} = \{1\} = f^{-1} (\{1\})\), and \(f^{-1} (1) \subseteq \{1\}\) holds.
3: Proof
Whole Strategy: Step 1: suppose that \(f^{-1} (s'_2) \cap S_1 \neq \emptyset\), and see that \(f^{-1} (s'_2) \subseteq S_1\).
Step 1:
Let us suppose that \(f^{-1} (s'_2) \cap S_1 \neq \emptyset\).
Let us suppose that \(s'_2 \notin S_2\).
\(f^{-1} (s'_2) \cap f^{-1} (S_2) = \emptyset\), by the proposition that the preimages of any disjoint subsets under any map are disjoint.
Let \(s_1 \in f^{-1} (s'_2) \cap S_1\) be any.
\(s_1 \in f^{-1} (s'_2) \cap S_1 = f^{-1} (S_2)\), a contradiction against \(f^{-1} (s'_2) \cap f^{-1} (S_2) = \emptyset\).
So, \(s'_2 \in S_2\).
So, \(f^{-1} (s'_2) \subseteq f^{-1} (S_2) = f^{-1} (s'_2) \cap S_1 \subseteq S_1\).
So, \(f^{-1} (s'_2) \cap S_1 = \emptyset\) or \(f^{-1} (s'_2) \subseteq S_1\).
