シーケンス（列）のサブシーケンス（部分列）の定義
話題
About: セット（集合）
この記事の目次
開始コンテキスト
- 読者は、シーケンス（列）の定義を知っている。
ターゲットコンテキスト
- 読者は、シーケンス（列）のサブシーケンス（部分列）の定義を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\( s\): \(\in \{\text{ 全てのシーケンス（列）たち }\}\)で、\(Dom (s) = J\)を満たすもの
\( J^`\): \(\subseteq \mathbb{N}\)
\( f\): \(: J^` \to J\)で、以下に指定されるコンディションたちを満たすもの
\(*s^`\): \(= s \circ f\), \(\in \{\text{ 全てのシーケンス（列）たち }\}\)で、\(Dom (s^`) = J^`\)を満たすもの
//
コンディションたち:
\(\forall j^`_1, j^`_2 \in J^` \text{ で、以下を満たすもの、つまり、 } 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: 注
したがって、\(J^` \subseteq J\)は要求されない、\(J^`\)はしばしば、\(J^` \subseteq J\)で\(f: j^` \mapsto j^`\)であるように選択されるもの。
当該コンディション\(\forall j \in J (\exists j^` \in J^` (j \le f (j^`)))\)は、例えば、\((s_2, s_2)\)を\((s_1, s_2, ...)\)に対して"サブシーケンス（部分列）"と呼ばないためのものである: もしも、\((s_2, s_2)\)が"サブシーケンス（部分列）"と呼ばれていたら、任意のシーケンス（列）はあるコンバージェント（収束する）サブシーケンス（部分列）を持つことになる、当該シーケンス（列）を単に有限に打ち切ることによって。
本定義によれば、\((s_1, s_2)\)に対して、\((s_2)\)はサブシーケンス（部分列）であるが、\((s_1)\)はそうではない。
\(\vert J \vert \in \mathbb{N}\)である時は、不可避に、\(\vert J^` \vert \in \mathbb{N}\)、なぜなら、以下を満たすある\(j^` \in J^`\)、つまり、\(J_{\vert J \vert} \le f (j^`)\)、があるところ、それは本当には\(J_{\vert J \vert} = f (j^`)\)、なぜなら、\(J_{\vert J \vert} = Max (J)\)、そして、\(j^` = Max (J^`)\)、なぜなら、もしも、以下を満たすある\(\widetilde{j^`} \in J^`\)、つまり、\(j^` \lt \widetilde{j^`}\)、があったら、\(Max (J) = J_{\vert J \vert} = f (j^`) \lt f (\widetilde{j^`})\)、矛盾、したがって、\(J^`_{\vert J^` \vert} = j^`\)および\(f (J^`_{\vert J^` \vert}) = J_{\vert J \vert}\)。
\(\vert J \vert = \infty\)である時は、不可避に、\(\vert J^` \vert = \infty\)、なぜなら、もしも、\(\vert J^` \vert \in \mathbb{N}\)であったら、以下を満たすある\(n \in \mathbb{N}\)、つまり、\(f (J^`_{\vert J^` \vert}) \lt J_n\)、があることになる、なぜなら、\(\vert J \vert = \infty\)、ところ、以下を満たすある\(n^` \in \mathbb{N}\)、つまり、\(J_n \le f (J^`_{n^`})\)、があることになる、したがって、\(f (J^`_{\vert J^` \vert}) \lt J_n \le f (J^`_{n^`})\)、しかし、\(J^`_{n^`} \le J^`_{\vert J^` \vert}\)であるから、\(f (J^`_{n^`}) \le f (J^`_{\vert J^` \vert})\)、矛盾。
各\(J^`_{n^`}\)に対して、\(f (J^`_{n^`}) = J_n\)、ここで、\(n^` \le n\)、であることを見よう。
それを、\(n^` \in \mathbb{N} \setminus \{0\}\)に関してインダクティブ（帰納的）に見よう。
\(n^` = 1\)である時は、\(f (J^`_1) = J_n\)、ここで、\(1 \le n\)、したがって、\(n^` = 1 \le n\)。
\(f (J^`_{n^`}) = J_n\)、ここで、\(n^` \le n\)、であると仮定しよう。
\(J^`_{n^`} \lt J^`_{n^` + 1}\)であるから、\(J_n = f (J^`_{n^`}) \lt f (J^`_{n^` + 1}) = J_{n'}\)、したがって、\(n \lt n'\)、したがって、\(n^` \le n \lt n'\)、したがって、\(n^` + 1 \le n'\)。
したがって、\(f (J^`_{n^`}) = J_n\)、ここで、\(n^` \le n\)、各\(n^` \in \mathbb{N} \setminus \{0\}\)に対して。
