description/proof of that for partially-ordered set and subset, if each element of subset is equal to or larger than element of set and infimum of subset exists, infimum is equal to or larger than element
Topics
About: set
The table of contents of this article
Starting Context
- 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 partially-ordered set and any subset, if each element of the subset is equal to or larger than any element of the set and the infimum of the subset exists, the infimum is equal to or larger than the 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 partially-ordered sets }\}\)
\(S\): \(\subseteq S'\)
\(s'\): \(\in S'\)
//
Statements:
(
\(\forall s \in S (s' \le s)\)
\(\land\)
\(\exists Inf (S)\)
)
\(\implies\)
\(s' \le Inf (S)\)
//
2: Proof
Whole Strategy: Step 1: see that \(s'\) is a lower bound of \(S\), and conclude the proposition.
Step 1:
\(s' \in Lb (S)\), by the definition of set of lower bounds of subset of partially-ordered set.
But \(Inf (S) = Max (Lb (S))\), by the definition of infimum of subset of partially-ordered set, which means that for each \(p \in Lb (S)\), \(p \le Inf (S)\), and as \(s'\) is such a \(p\), \(s' \le Inf (S)\).
