definition of canonical subsequence for subsequence of sequence
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 definition of canonical subsequence for 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\)
\( s^`\): \(\in \{\text{ the subsequences of } s\}\), \(= s \circ f\), where \(f: J^` \to J\) where \(J^` \subseteq \mathbb{N}\)
\(*\widetilde{s^`}\): \(\in \{\text{ the subsequences of } s\}\), \(= s \circ id_{f (J^`)}\), where \(id_{f (J^`)}: f (J^`) \to f (J^`)\) is the identity map
//
Conditions:
//
2: Note
\(\widetilde{s^`}\) seems a subsequence some people 1st imagine from "subsequence": for example, for a sequence, \(s: \mathbb{N} \to S\), choosing only the even-indexes elements, \(s \vert_{\{\text{ the even numbers }\}}: \{\text{ the even numbers }\} \to S = s \circ id_{\{\text{ the even numbers }\}}\) is certainly a subsequence.
The definition of subsequence of sequence is a generalization of such subsequences, but for each generalized subsequence, there is the corresponding canonical subsequence.
\(\widetilde{s^`}\) is indeed a subsequence, because \(\forall f (j^`_1), f (j^`_2) \in f (J^`) \text{ such that } f (j^`_1) \lt f (j^`_2) (id_{f (J^`)} (f (j^`_1)) = f (j^`_1) \lt f (j^`_2) = id_{f (J^`)} (f (j^`_2))) \land \forall j \in J (\exists f (j^`) \in f (J^`) (j \le f (j^`) = id_{f (J^`)} (f (j^`))))\).
