description/proof of that for linearly-ordered set and \(2\) elements, element is larger than 1st element and is equal to or larger than 2nd element iff this
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 description and a proof of the proposition that for any linearly-ordered set and any \(2\) elements, any elements is larger than the 1st element and is equal to or larger than the 2nd element if and only if (the 1st elements is smaller than the 2nd element and the element is equal to or larger than the 2nd element) or (the 2nd elements is equal to or smaller than the 1st element and the element is larger than the 1st element).
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 }\}\)
\(s_1\): \(\in S \cup \{- \infty\}\)
\(s'_1\): \(\in S\)
\(s\): \(\in S\)
//
Statements:
\(s_1 \lt s \land s'_1 \le s\)
\(\iff\)
\((s_1 \lt s'_1 \land s'_1 \le s) \lor (s'_1 \le s_1 \land s_1 \lt s)\)
//
\(- \infty \lt s\) means that \(s\) is not restricted by it; \(s'_1 \le - \infty\) never holds.
2: Note
\(s_1 \lt s \land s'_1 \lt s\) is easy to handle as \(Max (\{s_1, s'_1\}) \lt s\) and \(s_1 \le s \land s'_1 \le s\) is easy to handle as \(Max (\{s_1, s'_1\}) \le s\).
But \(s_1 \lt s \land s'_1 \le s\) is somewhat cumbersome and \((s_1 \lt s'_1 \land s'_1 \le s) \lor (s'_1 \le s_1 \land s_1 \lt s)\) is sometimes easier to handle.
3: Proof
Whole Strategy: Step 1: suppose that \(s_1 \lt s \land s'_1 \le s\); Step 2: see that \((s_1 \lt s'_1 \land s'_1 \le s) \lor (s'_1 \le s_1 \land s_1 \lt s)\); Step 3: suppose that \((s_1 \lt s'_1 \land s'_1 \le s) \lor (s'_1 \le s_1 \land s_1 \lt s)\); Step 4: see that \(s_1 \lt s \land s'_1 \le s\).
Step 1:
Let us suppose that \(s_1 \lt s \land s'_1 \le s\).
Step 2:
\(s_1 \lt s'_1\) or \(s'_1 \le s_1\).
When \(s_1 \lt s'_1\), \(s'_1 \le s\).
When \(s'_1 \le s_1\), \(s_1 \lt s\).
So, \((s_1 \lt s'_1 \land s'_1 \le s) \lor (s'_1 \le s_1 \land s_1 \lt s)\).
Step 3:
Let us suppose that \((s_1 \lt s'_1 \land s'_1 \le s) \lor (s'_1 \le s_1 \land s_1 \lt s)\).
Step 4:
When \(s_1 \lt s'_1 \land s'_1 \le s\), \(s_1 \lt s'_1 \le s\), so, \(s_1 \lt s\), so, \(s_1 \lt s \land s'_1 \le s\).
When \(s'_1 \le s_1 \land s_1 \lt s\), \(s'_1 \le s_1 \lt s\), so, \(s'_1 \lt s\), so, \(s'_1 \le s\), so, \(s_1 \lt s \land s'_1 \le s\).
So, \(s_1 \lt s \land s'_1 \le s\), anyway.
