definition of subsequence of sequence
Topics
About: set
The table of contents of this article
Starting Context
- The reader knows a definition of sequence.
Target Context
- The reader will have a definition of subsequence of sequence.
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 sequences }\}\), with \(Dom (s) = J\)
\( J^`\): \(\subseteq \mathbb{N}\)
\( f\): \(: J^` \to J\), which satisfies the conditions specified below
\(*s^`\): \(= s \circ f\), \(\in \{\text{ the sequences }\}\), with \(Dom (s^`) = J^`\)
//
Conditions:
\(\forall j^`_1, j^`_2 \in J^` \text{ such that } j^`_1 \lt j^`_2 (f (j^`_1) \lt f (j^`_2)) \land \forall j \in J (\exists j^` \in J^` (j \le f (j^`)))\)
//
2: Note
So, \(J^` \subseteq J\) is not required, although \(J^`\) is often chosen such that \(J^` \subseteq J\) with \(f: j^` \mapsto j^`\).
The condition, \(\forall j \in J (\exists j^` \in J^` (j \le f (j^`)))\), is for not calling \((s_2, s_2)\) for \((s_1, s_2, ...)\) "subsequence", for example: if \((s_2, s_2)\) was called "subsequence", any sequence would have a convergent subsequence just by truncating the sequence finitely.
According to this definition, for \((s_1, s_2)\), \((s_2)\) is a subsequence but \((s_1)\) is not.
When \(\vert J \vert \in \mathbb{N}\), inevitably, \(\vert J^` \vert \in \mathbb{N}\), because while there is a \(j^` \in J^`\) such that \(J_{\vert J \vert} \le f (j^`)\), it is really \(J_{\vert J \vert} = f (j^`)\), because \(J_{\vert J \vert} = Max (J)\), and \(j^` = Max (J^`)\), because if there was a \(\widetilde{j^`} \in J^`\) such that \(j^` \lt \widetilde{j^`}\), \(Max (J) = J_{\vert J \vert} = f (j^`) \lt f (\widetilde{j^`})\), a contradiction, so, \(J^`_{\vert J^` \vert} = j^`\) and \(f (J^`_{\vert J^` \vert}) = J_{\vert J \vert}\).
When \(\vert J \vert = \infty\), inevitably, \(\vert J^` \vert = \infty\), because if \(\vert J^` \vert \in \mathbb{N}\), while there would be an \(n \in \mathbb{N}\) such that \(f (J^`_{\vert J^` \vert}) \lt J_n\), because \(\vert J \vert = \infty\), there would be an \(n^` \in \mathbb{N}\) such that \(J_n \le f (J^`_{n^`})\), so, \(f (J^`_{\vert J^` \vert}) \lt J_n \le f (J^`_{n^`})\), but as \(J^`_{n^`} \le J^`_{\vert J^` \vert}\), \(f (J^`_{n^`}) \le f (J^`_{\vert J^` \vert})\), a contradiction.
Let us see that for each \(J^`_{n^`}\), \(f (J^`_{n^`}) = J_n\) where \(n^` \le n\).
Let us see that inductively with respect to \(n^` \in \mathbb{N} \setminus \{0\}\).
When \(n^` = 1\), \(f (J^`_1) = J_n\) where \(1 \le n\), so, \(n^` = 1 \le n\).
Let us suppose that \(f (J^`_{n^`}) = J_n\) where \(n^` \le n\).
As \(J^`_{n^`} \lt J^`_{n^` + 1}\), \(J_n = f (J^`_{n^`}) \lt f (J^`_{n^` + 1}) = J_{n'}\), so, \(n \lt n'\), so, \(n^` \le n \lt n'\), so, \(n^` + 1 \le n'\).
So, \(f (J^`_{n^`}) = J_n\) where \(n^` \le n\), for each \(n^` \in \mathbb{N} \setminus \{0\}\).
