description/proof of that for partially-ordered set and subset, if infimum of subset exists in subset, infimum is minimum of subset and if supremum of subset exists in subset, supremum is maximum of subset
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.
- The reader knows a definition of subset of partially-ordered set with induced partial ordering.
- The reader knows a definition of minimum of partially-ordered set.
- The reader knows a definition of supremum of subset of partially-ordered set.
- The reader knows a definition of maximum 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 the infimum of the subset exists in the subset, the infimum is the minimum of the subset and if the supremum of the subset exists in the subset, the supremum is the maximum of the subset.
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 }\}\), with any partial ordering, \(\lt'\)
\(S\): \(\subseteq S'\), with the induced partial ordering, \(\lt\)
//
Statements:
(
\(\exists Inf (S) \in S\)
\(\implies\)
\(Inf (S) = Min (S)\)
)
\(\land\)
(
\(\exists Sup (S) \in S\)
\(\implies\)
\(Sup (S) = Max (S)\)
)
//
2: Proof
Whole Strategy: Step 1: suppose that \(Inf (S)\) exists in \(S\); Step 2: see that \(Inf (S) = Min (S)\); Step 3: suppose that \(Sup (S)\) exists in \(S\); Step 4: see that \(Sup (S) = Max (S)\).
Step 1:
Let us suppose that \(Inf (S)\) exists in \(S\).
Step 2:
\(Inf (S) \in S\), by the supposition.
Let \(s \in S \setminus \{Inf (S)\}\) be any.
\(Inf (S) \lt' s\), because \(Inf (S) \in Lb (S)\).
\(Inf (S) \lt s\), by the definition of subset of partially-ordered set with induced partial ordering.
So, \(Inf (S) = Min (S)\)
Step 3:
Let us suppose that \(Sup (S)\) exists in \(S\).
Step 4:
\(Sup (S) \in S\), by the supposition.
Let \(s \in S \setminus \{Sup (S)\}\) be any.
\(s \lt' Sup (S)\), because \(Sup (S) \in Ub (S)\).
\(s \lt Sup (S)\), by the definition of subset of partially-ordered set with induced partial ordering.
So, \(Sup (S) = Max (S)\)
