description/proof of that for sequence on real numbers set with canonical ordering, if limit inferior and limit superior exist, limit inferior is equal to or smaller than limit superior
Topics
About: set
The table of contents of this article
Starting Context
- The reader knows a definition of limit inferior of sequence on partially-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, 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.
- The reader admits the proposition that for any non-decreasing sequence and any non-increasing sequence on any real numbers set with any same domain such that the 1st sequence is equal to or smaller than the 2nd sequence, each element of the 1st sequence is equal to or smaller than any element of the 2nd sequence, and the supremum of the 1st sequence is equal to or smaller than the infimum of 2nd sequence.
- The reader admits the proposition that for any partially-ordered set and any nonempty subset, if the infimum and the supremum of the subset exist, the infimum is equal to or smaller than the supremum.
Target Context
- The reader will have a description and a proof of the proposition that for any sequence on the real numbers set with the canonical ordering, if the limit inferior and the limit superior exist, the limit inferior is equal to or smaller than the 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\)
\(\mathbb{R}\): with the canonical ordering, \(\lt\)
\(s\): \(\in \{\text{ the sequences }\}\), such that \(Dom (s) = J\) and \(Ran (s) \subseteq \mathbb{R}\)
//
Statements:
\(\exists lim inf s \land \exists lim sup s\)
\(\implies\)
\(lim inf s \le lim sup s\)
//
2: Proof
Whole Strategy: Step 1: deal with the case that \(J\) is finite, and suppose otherwise thereafter; Step 2: apply the proposition that for any non-decreasing sequence and any non-increasing sequence on any real numbers set with any same domain such that the 1st sequence is equal to or smaller than the 2nd sequence, each element of the 1st sequence is equal to or smaller than any element of the 2nd sequence, and the supremum of the 1st sequence is equal to or smaller than the infimum of 2nd sequence.
Step 1:
Let us suppose that \(\vert J \vert = n \in \mathbb{N} \setminus \{0\}\).
\(lim inf s = s (J_n) = lim sup s\).
So, \(lim inf s \le lim sup s\).
Let us suppose otherwise hereafter.
Step 2:
\(Inf (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\})\) is non-decreasing with respect to \(m\) and \(Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\})\) is non-increasing with respect to \(m\), by 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.
\(Inf (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\}) \le Sup (\{s (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 nonempty subset, if the infimum and the supremum of the subset exist, the infimum is equal to or smaller than the supremum.
\(lim inf s = Sup (\{Inf (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\}) \vert m \in \mathbb{N} \setminus \{0\}\}) \le Inf (\{Sup (\{s (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\), by the proposition that for any non-decreasing sequence and any non-increasing sequence on any real numbers set with any same domain such that the 1st sequence is equal to or smaller than the 2nd sequence, each element of the 1st sequence is equal to or smaller than any element of the 2nd sequence, and the supremum of the 1st sequence is equal to or smaller than the infimum of 2nd sequence.
