definition of quotient set
Topics
About: set
The table of contents of this article
- Starting Context
- Target Context
- Orientation
- Main Body
- 1: Structured Description
- 2: Natural Language Description
- 3: Note
Starting Context
- The reader knows a definition of equivalence relation on set.
Target Context
- The reader will have a definition of quotient set.
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 }\}\)
\( \sim\): \(\in \{\text{ the equivalence relations on } S\}\)
\(*S / \sim\): \(= \{p \in Pow (S) \setminus \emptyset \vert \forall p', p'' \in p (p' \sim p'') \land \forall p' \in p, \forall p'' \in S \setminus p (\lnot p' \sim p'')\}\)
//
Conditions:
//
\(S / \sim\) is well-defined, because it is defined based on the subset axiom with a legitimate formula. Whether \(S / \sim\) partitions \(S\) is another issue, but \(S / \sim\) indeed partitions \(S\) as is shown in Note.
In other words, the quotient set is the set of the equivalence classes of \(S\) by \(\sim\).
2: Natural Language Description
For any set, \(S\), and any equivalence relation on \(S\), \( \sim\), \(S / \sim = \{p \in Pow (S) \setminus \emptyset \vert \forall p', p'' \in p (p' \sim p'') \land \forall p' \in p, \forall p'' \in S \setminus p (\lnot p' \sim p'')\}\)
3: Note
\(S / \sim\) is a partition of \(S\), which means that each element of \(S\) is contained in a single element of \(S / \sim\): for each \(p \in S\), there is the element of \(S / \sim\), \([p]\), defined by \(\{p' \in S \vert p' \sim p\}\), because for each \(p', p'' \in [p]\), \(p' \sim p\) and \(p'' \sim p\), which implies that \(p' \sim p''\), and for each \(p' \in [p], p'' \in S \setminus [p]\), \(p \sim p'\) and \(\lnot p \sim p''\), which implies that \(\lnot p' \sim p''\), because if \(p' \sim p''\), \(p \sim p''\), a contradiction; \(p\) does not belong to any other element of \(S / \sim\), because if \(p\) belonged to another element, \([p'] \in S / \sim\), for each element, \(p'' \in [p']\), \(p'' \sim p\), which would mean that \(p'' \in [p]\), and for each element, \(p'' \in [p]\), \(p'' \sim p\), which would mean that \(p'' \in [p']\), so, \([p'] = [p]\) after all.
