description/proof of that for linearly-ordered set and subset, element of set is supremum of subset iff element is equal to or larger than each element of subset and for each element of set smaller than element, there is element of subset larger
Topics
About: set
The table of contents of this article
Starting Context
- The reader knows a definition of linearly-ordered set.
- The reader knows a definition of supremum of subset of partially-ordered set.
Target Context
- The reader will have a description and a proof of the proposition that for any linearly-ordered set and any subset, any element of the set is the supremum of the subset if and only if the element is equal to or larger than each element of the subset and for each element of the set smaller than the element, there is an element of the subset larger.
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'\)
\(s'\): \(\in S'\)
//
Statements:
\(s' = Sup (S)\)
\(\iff\)
\((\forall s \in S (s \le s')) \land (\forall s'' \in S' \text{ such that } s'' \lt' s' (\exists s \in S (s'' \lt' s)))\)
//
2: Note
This proposition holds (vacuously) even when \(S = \emptyset\).
3: Proof
Whole Strategy: Step 1: suppose that \(s' = Sup (S)\); Step 2: see that \((\forall s \in S (s \le s')) \land (\forall s'' \in S' \text{ such that } s'' \lt' s' (\exists s \in S (s'' \lt' s)))\); Step 3: suppose that \((\forall s \in S (s \le s')) \land (\forall s'' \in S' \text{ such that } s'' \lt' s' (\exists s \in S (s'' \lt' s)))\); Step 4: see that \(s' = Sup (S)\); Step 5: check that this proposition holds even when \(S = \emptyset\).
Step 1:
Let us suppose that \(s' = Sup (S)\).
Step 2:
Let \(s \in S\) be any.
As \(Sup (S) \in Ub (S)\), \(s \le s'\), by the definition of set of upper bounds.
So, \(\forall s \in S (s \le s')\).
Let \(s'' \in S'\) be any such that \(s'' \lt' s'\).
Let us suppose that there was no \(s \in S\) such that \(s'' \lt' s\).
That would mean that for each \(s \in S\), \(s \le' s''\), because \(S'\) was linearly-ordered.
That would mean that \(s'' \in Ub (S)\).
But as \(s'' \lt' s'\), \(s'\) was not the minimum of \(Ub (S)\), a contradiction against \(s' = Sup (S)\).
So, there is an \(s \in S\) such that \(s'' \lt' s\).
Step 3:
Let us suppose that \((\forall s \in S (s \le s')) \land (\forall s'' \in S' \text{ such that } s'' \lt' s' (\exists s \in S (s'' \lt' s)))\).
Step 4:
\(s' \in Ub (S)\), by the definition of set of upper bounds.
Let us suppose \(s'\) was not the minimum of \(Ub (S)\).
That would means that there was an \(s'' \in Ub (S)\) such that \(s' \le' s''\) did not hold.
As \(S'\) was linearly-ordered, \(s'' \lt' s'\).
By the supposition, there would be an \(s \in S\) such that \(s'' \lt' s\), which would mean that \(s \le' s''\) would not hold.
That would mean that \(s'' \notin Ub (S)\), a contradiction against \(s'' \in Ub (S)\).
So, \(s'\) is the minimum of \(Ub (S)\).
So, \(s' = Sup (S)\).
Step 5:
Let us check that this proposition holds even when \(S = \emptyset\).
\(Ub (S) = S'\).
\(Sup (S) = Min (Ub (S)) = Min (S')\).
So, if \(s' = Sup (S)\), \(\forall s \in S (s \le s')\) vacuously holds and \(\forall s'' \in S' \text{ such that } s'' \lt' s' (\exists s \in S (s'' \lt' s))\) vacuously holds: there is no such \(s''\).
If \((\forall s \in S (s \le s')) \land (\forall s'' \in S' \text{ such that } s'' \lt' s' (\exists s \in S (s'' \lt' s)))\) holds, there is no such \(s''\), because otherwise, \(\exists s \in S (s'' \lt' s)\) would not hold, so, \(s' = Min (S') = Sup (S)\).
