description/proof of that for linearly-ordered set and subset, element of set is infimum of subset iff element is equal to or smaller than each element of subset and for each element of set larger than element, there is element of subset smaller
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 infimum 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 infimum of the subset if and only if the element is equal to or smaller than each element of the subset and for each element of the set larger than the element, there is an element of the subset smaller.
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' = Inf (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' = Inf (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' = Inf (S)\); Step 5: check that this proposition holds even when \(S = \emptyset\).
Step 1:
Let us suppose that \(s' = Inf (S)\).
Step 2:
Let \(s \in S\) be any.
As \(Inf (S) \in Lb (S)\), \(s' \le s\), by the definition of set of lower 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 Lb (S)\).
But as \(s' \lt' s''\), \(s'\) was not the maximum of \(Lb (S)\), a contradiction against \(s' = Inf (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 Lb (S)\), by the definition of set of lower bounds.
Let us suppose \(s'\) was not the maximum of \(Lb (S)\).
That would means that there was an \(s'' \in Lb (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 Lb (S)\), a contradiction against \(s'' \in Lb (S)\).
So, \(s'\) is the maximum of \(Lb (S)\).
So, \(s' = Inf (S)\).
Step 5:
Let us check that this proposition holds even when \(S = \emptyset\).
\(Lb (S) = S'\).
\(Inf (S) = Max (Lb (S)) = Max (S')\).
So, if \(s' = Inf (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' = Max (S') = Inf (S)\).
