description/proof of that for real numbers field with canonical linear ordering and finite set of subsets, if sum of each set of representatives of subsets is equal to or larger than number, sum of infimums of subsets is equal to or larger than number
Topics
About: set
The table of contents of this article
Starting Context
- The reader knows a definition of real numbers field.
- The reader knows a definition of infimum of subset of partially-ordered set.
- The reader admits 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.
Target Context
- The reader will have a description and a proof of the proposition that for the real numbers field with the canonical linear ordering and any finite set of subsets, if the sum of each set of representatives of the subsets is equal to or larger than any number, the sum of the infimums of the subsets is equal to or larger than the number.
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:
\(\mathbb{R}\): \(= \text{ the real numbers field with the canonical linear ordering }\)
\(J\): \(\in \{\text{ the finite index sets }\}\), with \(\vert J \vert = n\)
\(\{S_j \subseteq \mathbb{R} \vert j \in J\}\):
\(r\): \(\in \mathbb{R}\)
//
Statements:
\(\forall s \in \times_{j \in J} S_j (r \le \sum_{j \in J} s^j)\)
\(\implies\)
\(r \le \sum_{j \in J} Inf (S_j)\)
//
\(Inf (S_j)\) s inevitably exist.
2: Proof
Whole Strategy: Step 1: see that each \(Inf (S_j)\) exists; Step 2: suppose that \(\sum_{j \in J} Inf (S_j) \lt r\) and find a contradiction.
Step 1:
Let us see that each \(Inf (S_l)\) exists.
Let \(s^m\) be fixed for each \(m \in J \setminus \{l\}\).
For each \(p \in S_l\), \(r \le \sum_{j \in J \setminus \{l\}} s^j + p\).
So, for each \(p \in S_l\), \(r - \sum_{j \in J \setminus \{l\}} s^j \le p\).
So, \(S_l\) is lower bounded, and \(Inf (S_l)\) exists, because any lower bounded subset of \(\mathbb{R}\) has the infimum, as is well known.
Step 2:
Let us suppose that \(\sum_{j \in J} Inf (S_j) \lt r\).
Let \(\epsilon := (r - \sum_{j \in J} Inf (S_j)) / (2 n)\).
For each \(j \in J\), there would be a \(p_j \in S_j\) such that \(p_j \lt Inf (S_j) + \epsilon\), by 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.
Let \(s \in \times_{j \in J} S_j\) be the one such that for each \(j \in J\), \(s^j = p_j\).
\(\sum_{j \in J} s^j \lt \sum_{j \in J} (Inf (S_j) + \epsilon) = \sum_{j \in J} Inf (S_j) + n \epsilon = \sum_{j \in J} Inf (S_j) + (r - \sum_{j \in J} Inf (S_j)) / 2 \lt r\), a contradiction.
So, \(r \le \sum_{j \in J} Inf (S_j)\).
