description/proof of that for infinite sequence, subsequence is infinite
Topics
About: set
The table of contents of this article
Starting Context
- The reader knows a definition of subsequence of sequence.
Target Context
- The reader will have a description and a proof of the proposition that for any infinite sequence, any subsequence is infinite.
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\) such that \(J \in \{\text{ the infinite sets }\}\)
\(s^`\): \(= s \circ f\), \(\in \{\text{ the subsequences of } s\}\), with \(dom s^` = J^`\)
//
Statements:
\(J^` \in \{\text{ the infinite sets }\}\)
//
2: Note
This is because of our definition of subsequence of sequence, which requires that \(\forall j \in J (\exists j^` \in J^` (j \le f (j^`)))\): for example, for \((s_0, s_1, ...)\), \((s_0, s_1)\) is not called "subsequence" by our definition.
3: Proof
Whole Strategy: Step 1: suppose that \(J^` = \{j_1, ..., j_n\}\) and find a contradiction.
Step 1:
Let us suppose that \(J^`\) was finite, \(= \{j_1, ..., j_n\}\), in the ascending order.
\(f (j_n) \in J \subseteq \mathbb{N}\).
As \(J\) was infinite, there would be a \(j \in J\) such that \(f (j_n) \lt j\).
But there would be no \(j^` \in J^`\) such that \(j \le f (j^`)\), because while \(f (j_n) \lt j\), for each \(j_l \in J^`\) such that \(l \lt n\), \(f (j_l) \lt f (j_n) \lt j\), a contradiction against \(s^`\)'s being a subsequence.
So, \(J^`\) is infinite.
