definition of subset of linearly-ordered set with induced linear ordering
Topics
About: set
The table of contents of this article
Starting Context
- The reader knows a definition of linearly-ordered set.
Target Context
- The reader will have a definition of subset of linearly-ordered set with induced linear ordering.
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 linearly-ordered sets }\}\) with any linear ordering, \(\lt'\)
\(*S\): \(\subseteq S'\) with the linear ordering, \(\lt := \lt' \cap (S \times S)\)
//
Conditions:
//
2: Note
Let us see that \(\lt\) is indeed a linear ordering.
Note that any linear ordering is a relation, which is a set of some ordered pairs.
\(\lt' \subseteq S' \times S'\).
So, \(\lt' \cap (S \times S)\) makes sense, and \(\lt \subseteq S \times S\) is a relation.
Let us see that \(\lt\) satisfies the conditions to be a linear ordering.
1) \(\lt\) is a trichotomy for any element, \(s_1 \in S\): for any element, \(s_2, \in S\), exclusively \(s_1 \lt s_2\), \(s_1 = s_2\), or \(s_2 \lt s_1\), because as \(s_1, s_2 \in S'\), exclusively, \(s_1 \lt' s_2\), \(s_1 = s_2\), or \(s_2 \lt' s_1\), which means that exclusively, \((s_1, s_2) \in \lt'\), \(s_1 = s_2\), or \((s_2, s_1) \in \lt'\), which implies that exclusively, \((s_1, s_2) \in \lt' \cap (S \times S) = \lt\), \(s_1 = s_2\), or \((s_2, s_1) \in \lt' \cap (S \times S) = \lt\), which means that exclusively, \(s_1 \lt s_2\), \(s_1 = s_2\), or \(s_2 \lt s_1\).
2) \(\lt\) is transitive: for any elements, \(s_1, s_2, s_3 \in S\), such that \(s_1 \lt s_2\) and \(s_2 \lt s_3\), \(s_1 \lt s_3\), because while \(s_1, s_2, s_3 \in S'\), \(s_1 \lt s_2\) and \(s_2 \lt s_3\) means that \((s_1, s_2) \in \lt = \lt' \cap (S \times S)\) and \((s_2, s_3) \in \lt = \lt' \cap (S \times S)\), which implies that \((s_1, s_2) \in \lt'\) and \((s_2, s_3) \in \lt'\), which means that \(s_1 \lt' s_2\) and \(s_2 \lt' s_3\), so, \(s_1 \lt' s_3\), which means that \((s_1, s_3) \in \lt'\), so, \((s_1, s_3) \in \lt' \cap (S \times S) = \lt\), which means that \(s_1 \lt s_3\).
