description/proof of that for linearly-ordered set and \(2\) elements, element is smaller than 1st element and is smaller than 2nd element iff element is smaller than minimum of \(2\) elements
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 element is smaller than the 1st element and is smaller than the 2nd element if and only if the element is smaller than the minimum of the \(2\) elements.
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_2\): \(\in S \cup \{\infty\}\)
\(s'_2\): \(\in S \cup \{\infty\}\)
\(s\): \(\in S\)
//
Statements:
\(s \lt s_2 \land s \lt s'_2\)
\(\iff\)
\(s \lt Min (\{s_2, s'_2\})\)
//
Each of \(s \lt \infty\) and \(s \le \infty\) means that \(s\) is not restricted by it; \(Max (\{\infty, s\}) := s\) and \(Max (\{\infty, \infty\}) := \infty\).
2: Proof
Whole Strategy: Step 1: suppose that \(s \lt s_2 \land s \lt s'_2\); Step 2: see that \(s \lt Min (\{s_2, s'_2\})\); Step 3: suppose that \(s \lt Min (\{s_2, s'_2\})\); Step 4: see that \(s \lt s_2 \land s \lt s'_2\).
Step 1:
Let us suppose that \(s \lt s_2 \land s \lt s'_2\).
Step 2:
\(Min (\{s_2, s'_2\}) = s_2 \text{ or } s'_2\).
When \(Min (\{s_2, s'_2\}) = s_2\), \(s \lt s_2 = Min (\{s_2, s'_2\})\).
When \(Min (\{s_2, s'_2\}) = s'_2\), \(s \lt s'_2 = Min (\{s_2, s'_2\})\).
So, \(s \lt Min (\{s_2, s'_2\})\), anyway.
Step 3:
Let us suppose that \(s \lt Min (\{s_2, s'_2\})\).
Step 4:
When \(s_2 = s'_2 = \infty\), \(s \lt s_2 \land s \lt s'_2\).
Let us suppose otherwise, hereafter.
\(s \lt Min (\{s_2, s'_2\}) \le s_2, s'_2\).
So, \(s \lt s_2 \land s \lt s'_2\).
