description/proof of that for \(2\) sequences with same domain on linearly-ordered set that have limits superior, if latter sequence is equal to or larger than former, latter limit superior is equal to or larger than former limit superior
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 limit superior of sequence on partially-ordered set.
- The reader admits the proposition that for any partially-ordered set and any subset, if the minimum of the subset exists, the minimum is the infimum of the subset, and if the maximum of the subset exists, the maximum is the supremum of the subset.
- The reader admits the proposition that for any partially-ordered set, any subset, and any subset of the subset, if the infimum of the subset and the infimum of the subset of the subset exist, the infimum of the subset is equal to or smaller than the infimum of the subset of the subset, and if the supremum of the subset and the supremum of the subset of the subset exist, the supremum of the subset is equal to or larger than the supremum of the subset of the subset.
Target Context
- The reader will have a description and a proof of the proposition that for any \(2\) sequences with any same domain on any linearly-ordered set that have any limits superior, if the latter sequence is equal to or larger than the former sequence, the latter limit superior is equal to or larger than the former limit superior.
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:
\(J\): \(\subseteq \mathbb{N}\), such that \(J \neq \emptyset\)
\(S\): \(\in \{\text{ the linearly-ordered sets }\}\) with any linear ordering, \(\lt\)
\(s_1\): \(: J \to S\), such that \(\exists lim sup s_1\)
\(s_2\): \(: J \to S\), such that \(\exists lim sup s_2\)
//
Statements:
\(\forall j \in J (s_1 (j) \le s_2 (j))\)
\(\implies\)
\(lim sup s_1 \le lim sup s_2\)
//
2: Proof
Whole Strategy: Step 1: deal with the case that \(J\) is finite, and suppose otherwise, thereafter; Step 2: see that \(Sup (\{s_1 (J_n) \vert m \le n\}) \le Sup (\{s_2 (J_n) \vert m \le n\})\); Step 3: see that \(Inf (\{Sup (\{s_1 (J_n) \vert m \le n\})\}) \le Inf (\{Sup (\{s_2 (J_n) \vert m \le n\})\})\).
Step 1:
When \(\vert J \vert = n \in \mathbb{N} \setminus \{0\}\), \(lim sup s_1 = s_1 (J_n) \le s_2 (J_n) = lim sup s_2\).
Let us suppose otherwise, hereafter.
Step 2:
\(Ub (\{s_2 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\}) \subseteq Ub (\{s_1 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\})\), because for each \(s \in Ub (\{s_2 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\})\), for each \(n \in \mathbb{N} \setminus \{0\}\) such that \(m \le n\), \(s_2 (J_n) \le s\), so, \(s_1 (J_n) \le s\), so, \(s \in Ub (\{s_1 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\})\).
So, \(Sup (\{s_1 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\}) = Min (Ub (\{s_1 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\})) \le Min (Ub (\{s_2 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\})) = Sup (\{s_2 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\})\), by the proposition that for any partially-ordered set and any subset, if the minimum of the subset exists, the minimum is the infimum of the subset, and if the maximum of the subset exists, the maximum is the supremum of the subset and the proposition that for any partially-ordered set, any subset, and any subset of the subset, if the infimum of the subset and the infimum of the subset of the subset exist, the infimum of the subset is equal to or smaller than the infimum of the subset of the subset, and if the supremum of the subset and the supremum of the subset of the subset exist, the supremum of the subset is equal to or larger than the supremum of the subset of the subset.
Step 3:
\(Lb (\{Sup (\{s_1 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\}) \vert m \in \mathbb{N} \setminus \{0\}\}) \subseteq Lb (\{Sup (\{s_2 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\}) \vert m \in \mathbb{N} \setminus \{0\}\})\), because for each \(s \in Lb (\{Sup (\{s_1 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\}) \vert m \in \mathbb{N} \setminus \{0\}\})\), \(s \le Sup (\{s_1 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\})\) for each \(m \in \mathbb{N} \setminus \{0\}\), so, \(s \le Sup (\{s_1 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\}) \le Sup (\{s_2 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\})\), by Step 2, so, \(s \in Lb (\{Sup (\{s_2 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\}) \vert m \in \mathbb{N} \setminus \{0\}\})\).
\(lim sup s_1 = Inf (\{Sup (\{s_1 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\}) \vert m \in \mathbb{N} \setminus \{0\}\}) = Max (Lb (\{Sup (\{s_1 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\}) \vert m \in \mathbb{N} \setminus \{0\}\})) \le Max (Lb (\{Sup (\{s_2 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\}) \vert m \in \mathbb{N} \setminus \{0\}\})) = Inf (\{Sup (\{s_2 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\}) \vert m \in \mathbb{N} \setminus \{0\}\}) = lim sup s_2\), by the proposition that for any partially-ordered set and any subset, if the minimum of the subset exists, the minimum is the infimum of the subset, and if the maximum of the subset exists, the maximum is the supremum of the subset and the proposition that for any partially-ordered set, any subset, and any subset of the subset, if the infimum of the subset and the infimum of the subset of the subset exist, the infimum of the subset is equal to or smaller than the infimum of the subset of the subset, and if the supremum of the subset and the supremum of the subset of the subset exist, the supremum of the subset is equal to or larger than the supremum of the subset of the subset.
