メトリックスペース（計量付き空間）上のコンバージェント（収束する）シーケンス（列）に対して、サブシーケンス（部分列）はシーケンス（列）のコンバージェンス（収束ポイント）へコンバージ（収束）することの記述/証明
話題
About: メトリックスペース（計量付き空間）
この記事の目次
開始コンテキスト
- 読者は、メトリックスペース（計量付き空間）上のシーケンス（列）のコンバージェンス（収束ポイント）の定義を知っている。
- 読者は、シーケンス（列）のサブシーケンス（部分列）の定義を知っている。
ターゲットコンテキスト
- 読者は、任意のメトリックスペース（計量付き空間）上の任意のコンバージェント（収束する）シーケンス（列）に対して、その任意のサブシーケンス（部分列）は当該シーケンス（列）のコンバージェンス（収束ポイント）へコンバージ（収束）するという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(J\): \(\subseteq \mathbb{N}\)で、以下を満たすもの、つまり、\(J \neq \emptyset\)
\(M\): \(\in \{\text{ 全てのメトリックスペース（計量付き空間）たち }\}\)
\(s\): \(\in \{\text{ 全てのシーケンス（列）たち }\}\)で、以下を満たすもの、つまり、\(Dom (s) = J\)および\(Ran (s) \subseteq M\)
\(J^`\): \(\subseteq \mathbb{N}\)で、以下を満たすもの、つまり、\(J^` \neq \emptyset\)
\(s^`\): \(= s \circ f\), \(\in \{s \text{ の全てのサブシーケンス（部分列）たち } \text{ で、 } f: J^` \to J\} \text{ を持つもの }\)
//
ステートメント（言明）たち:
\(\exists lim s\)
\(\implies\)
\(\exists lim s^` \land lim s^` = lim s\)
//
2: 注
任意のパーシャリーオーダードセット（半順序集合）上の任意のシーケンス（列）および任意のサブシーケンス（部分列）に対して、もしも、当該シーケンス（列）のリミットインフェリア（下極限）が存在する場合、当該サブシーケンス（部分列）のリミットインフェリア（下極限）は必ずしも存在せず、もしも、それが存在する場合、それは当該シーケンス（列）のリミットインフェリア（下極限）以上であるという命題および任意のパーシャリーオーダードセット（半順序集合）上の任意のシーケンス（列）および任意のサブシーケンス（部分列）に対して、もしも、当該シーケンス（列）のリミットスピアリア（上極限）が存在する場合、当該サブシーケンス（部分列）のリミットスピアリア（上極限）は必ずしも存在せず、もしも、それが存在する場合、それは当該シーケンス（列）のリミットスピアリア（上極限）以下であるという命題と比較のこと。
3: 証明
全体戦略: ステップ1: \(J\)がファイナイト（有限）であるケースに対処し、それ以降は、そうでないと仮定する; ステップ2: 以下を満たす\(N\)、つまり、各\(N \lt n\)に対して、\(dist (lim s, s (J_n)) \lt \epsilon\)、を取り、以下を満たす\(N^`\)、つまり、\(N \le f (N^`)\)、を取り、各\(N^` \lt n\)に対して、\(dist (lim s, s^` (J^`_n)) \lt \epsilon\)であることを見る。
ステップ1:
\(\vert J \vert \in \mathbb{N} \setminus \{0\}\)であると仮定しよう。
\(lim s = s (J_{\vert J \vert})\)、定義によって。
\(\vert J^` \vert \in \mathbb{N} \setminus \{0\}\)、シーケンス（列）のサブシーケンス（部分列）の定義に対する"注"によって。
\(lim s^` = s^` (J^`_{\vert J^` \vert}) = s \circ f (J^`_{\vert J^` \vert}) = s (J_{\vert J \vert}) = lim s\)。
これ以降は、そうでないと仮定しよう。
ステップ2:
\(\epsilon \in \mathbb{R}\)を、\(0 \lt \epsilon\)を満たす任意のものとしよう。
以下を満たすある\(N \in \mathbb{N} \setminus \{0\}\)、つまり、\(N \lt n\)を満たす各\(n \in \mathbb{N} \setminus \{0\}\)に対して、\(dist (lim s, s (J_n)) \lt \epsilon\)、がある。
以下を満たすある\(N^` \in \mathbb{N} \setminus \{0\}\)、つまり、\(J_N \le f (J^`_{N^`})\)、がある。
\(N^` \lt n^`\)を満たす各\(n^` \in \mathbb{N} \setminus \{0\}\)に対して、\(f (J^`_{N'}) \lt f (J^`_{n^`})\)、したがって、\(J_N \le f (J^`_{N^`}) \lt f (J^`_{n^`})\)、ここで、\(f (J^`_{n^`}) = J_n\)で\(N \lt n\)を満たす、したがって、\(dist (lim s, s^` (J^`_{n^`})) = dist (lim s, s \circ f (J^`_{n^`})) = dist (lim s, s (J_n)) \lt \epsilon\)。
したがって、\(lim s^` = lim s\)。
