description/proof of that saturation of subset of set with equivalence relation is subset iff subset is union of equivalence classes
Topics
About: set
The table of contents of this article
Starting Context
- The reader knows a definition of saturation of subset of set with equivalence relation.
Target Context
- The reader will have a description and a proof of the proposition that the saturation of any subset of any set with any equivalence relation is the subset iff the subset is the union of some equivalence classes.
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'\): \(\in \{\text{ the sets }\}\), with any equivalence relation, \(\sim'\)
\(S\): \(\subseteq S'\)
//
Statements:
\(Sat (S, \sim') = S\)
\(\iff\)
\(\exists \widetilde{S} \subseteq S' / \sim' (S = \cup \widetilde{S})\)
//
2: Proof
Whole Strategy: Step 1: suppose that \(Sat (S, \sim') = S\); Step 2: see that \(S\) is the union of some equivalence classes; Step 3: suppose that \(S\) is the union of some equivalence classes; Step 4: see that \(Sat (S, \sim') = S\).
Step 1:
Let us suppose that \(Sat (S, \sim') = S\).
Step 2:
Let \(s \in S\) be any.
\([s]' \subseteq S\), because otherwise, there would be an \(s' \in [s]' \setminus S\), so, \(s' \sim' s\), so, \(s' \in Sat (S, \sim')\) while \(s' \notin S\), a contradiction against \(Sat (S, \sim') = S\).
Then, \(S = \cup_{s \in S} [s]'\), because for each \(s \in S\), \(s \in \cup_{s \in S} [s]'\); for each \(s' \in \cup_{s \in S} [s]'\), \(s' \in [s]'\) for an \(s \in S\), but \([s]' \subseteq S\), as has been seen above, so, \(s' \in [s]' \subseteq S\).
So, for \(\widetilde{S} := \{[s]' \vert s \in S\} \subseteq S' / \sim'\), \(S = \cup \widetilde{S}\): of course, \(\{[s]' \vert s \in S\}\) may have some duplications.
Step 3:
Let us suppose that \(S\) is the union of some equivalence classes: \(S = \cup \widetilde{S}\).
Step 4:
For each \(s' \in S' \setminus S\), \(s' \notin Sat (S, \sim')\) (so, \(s' \in S' \setminus Sat (S, \sim')\)), because otherwise, there would an \(s \in S\) such that \(s \sim' s'\), which would mean that \(s' \in [s]'\), so, \([s]' \notin \widetilde{S}\), because otherwise, \(\cup \widetilde{S}\) would contain \(s' \notin S\), a contradiction against \(S = \cup \widetilde{S}\), but \([s]' \in \widetilde{S}\), because otherwise, \(s \notin \cup \widetilde{S} = S\), because \(S' / \sim'\) was a partition of \(S'\), a contradiction, a contradiction against \([s]' \notin \widetilde{S}\).
So, \(S' \setminus S \subseteq S' \setminus Sat (S, \sim')\), so, \(Sat (S, \sim') \subseteq S\).
As \(S \subseteq Sat (S, \sim')\), as is mentioned in Note for the definition of saturation of subset of set with equivalence relation, \(Sat (S, \sim') = S\).
