メトリックスペース（計量付き空間）に対して、もしも、その上の各シーケンス（列）がコンバージェント（収束する）サブシーケンス（部分列）を持つ場合、そしてその場合に限って、その上のナチュラルナンバー（自然数）たちセット（集合）からの各シーケンス（列）はコンバージェント（収束する）サブシーケンス（部分列）を持つことの記述/証明
話題
About: メトリックスペース（計量付き空間）
この記事の目次
開始コンテキスト
ターゲットコンテキスト
- 読者は、任意のメトリックスペース（計量付き空間）に対して、もしも、その上の各シーケンス（列）があるコンバージェント（収束する）サブシーケンス（部分列）を持つ場合、そしてその場合に限って、その上のナチュラルナンバー（自然数）たちセット（集合）からの各シーケンス（列）はあるコンバージェント（収束する）サブシーケンス（部分列）を持つという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(M\): \(\in \{\text{ 全てのメトリックスペース（計量付き空間）たち }\}\)
//
ステートメント（言明）たち:
\(\forall s: J \to M \in \{\text{ 全てのシーケンス（列）たち }\} (\exists s^`: J^` \to M \in \{s \text{ の全てのサブシーケンス（部分列）たち }\} (s^` \in \{\text{ 全てのコンバージェント（収束する）シーケンス（列）たち }\}))\)
\(\iff\)
\(\forall s: \mathbb{N} \to M \in \{\text{ 全てのシーケンス（列）たち }\} (\exists s^`: J^` \to M \in \{s \text{ の全てのサブシーケンス（部分列）たち }\} (s^` \in \{\text{ 全てのコンバージェント（収束する）シーケンス（列）たち }\}))\)
\(\iff\)
\(\forall s: \mathbb{N} \to M \in \{\text{ 全てのシーケンス（列）たち }\} (\exists s^`: \mathbb{N} \to M \in \{s \text{ の全てのサブシーケンス（部分列）たち }\} (s^` \in \{\text{ 全てのコンバージェント（収束する）シーケンス（列）たち }\}))\)
//
2: 証明
全体戦略: ステップ0: \(\forall s: J \to M \in \{\text{ 全てのシーケンス（列）たち }\} (\exists s^`: J^` \to M \in \{s \text{ の全てのサブシーケンス（部分列）たち }\} (s^` \in \{\text{ 全てのコンバージェント（収束する）シーケンス（列）たち }\}))\)を、"ステートメント（言明）A"と呼ぶ、\(\forall s: \mathbb{N} \to M \in \{\text{ 全てのシーケンス（列）たち }\} (\exists s^`: J^` \to M \in \{s \text{ の全てのサブシーケンス（部分列）たち }\} (s^` \in \{\text{ 全てのコンバージェント（収束する）シーケンス（列）たち }\}))\)を、"ステートメント（言明）B"と呼ぶ、\(\forall s: \mathbb{N} \to M \in \{\text{ 全てのシーケンス（列）たち }\} (\exists s^`: \mathbb{N} \to M \in \{s \text{ の全てのサブシーケンス（部分列）たち }\} (s^` \in \{\text{ 全てのコンバージェント（収束する）シーケンス（列）たち }\}))\)を、"ステートメント（言明）C"と呼ぶ; ステップ1: ステートメント（言明）Aを仮定する; ステップ2: ステートメント（言明）Bが成立することを見る; ステップ3: ステートメント（言明）Bを仮定する; ステップ4: ステートメント（言明）Cが成立することを見る; ステップ5: ステートメント（言明）Cを仮定する; ステップ6: ステートメント（言明）Aが成立することを見る。
ステップ0:
\(\forall s: J \to M \in \{\text{ 全てのシーケンス（列）たち }\} (\exists s^`: J^` \to M \in \{s \text{ の全てのサブシーケンス（部分列）たち }\} (s^` \in \{\text{ 全てのコンバージェント（収束する）シーケンス（列）たち }\}))\)を、"ステートメント（言明）A"と呼ぼう。
\(\forall s: \mathbb{N} \to M \in \{\text{ 全てのシーケンス（列）たち }\} (\exists s^`: J^` \to M \in \{s \text{ の全てのサブシーケンス（部分列）たち }\} (s^` \in \{\text{ 全てのコンバージェント（収束する）シーケンス（列）たち }\}))\)を、"ステートメント（言明）B"と呼ぼう。
\(\forall s: \mathbb{N} \to M \in \{\text{ 全てのシーケンス（列）たち }\} (\exists s^`: \mathbb{N} \to M \in \{s \text{ の全てのサブシーケンス（部分列）たち }\} (s^` \in \{\text{ 全てのコンバージェント（収束する）シーケンス（列）たち }\}))\)を、"ステートメント（言明）C"と呼ぼう。
ステップ1:
ステートメント（言明）Aを仮定しよう。
ステップ2:
各\(s: \mathbb{N} \to M\)はある\(s: J \to M\)である、したがって、あるコンバージェント（収束する）\(s^`: J^` \to M\)がある、ステートメント（言明）Aによって、したがって、ステートメント（言明）Bは成立する。
ステップ3:
ステートメント（言明）Bを仮定しよう。
ステップ4:
\(s: \mathbb{N} \to M\)を任意のものとしよう。
ステートメント（言明）Bによって、あるコンバージェント（収束する）\(s^`: J^` \to M\)がある、それが意味するのは、\(s^` = s \circ f\)。
注意として、\(J^`\)は不可避に、あるインフィニット（無限）セット（集合）である、シーケンス（列）のサブシーケンス（部分列）の定義に対する"注"によって。
順序維持バイジェクション（全単射）\(g: J^` \to \mathbb{N}, {J^`}_n \mapsto n - 1\)がある、それは、本当に、順序維持である、なぜなら、各\({J^`}_n \lt {J^`}_{n'}\)に対して、\(n \lt n'\)、したがって、\(n - 1 \lt n' - 1\); それは、本当に、あるバイジェクション（全単射）である、なぜなら、各\({J^`}_n \neq {J^`}_{n'}\)に対して、\(n \neq n'\)、したがって、\(n - 1 \neq n' - 1\)、そして、各\(n \in \mathbb{N}\)に対して、\({J^`}_{n + 1}\)は\(n\)へマップされる。
注意として、\(g^{-1}\)も順序維持である、なぜなら、各\(n \lt n'\)に対して、\(g^{-1} (n) = {J^`}_{n + 1} \lt {J^`}_{n' + 1} = g^{-1} (n')\)。
\(\widetilde{s^`}: \mathbb{N} \to M = s^` \circ g^{-1} = s \circ f \circ g^{-1}\)としよう。
\(\widetilde{s^`}\)は\(s\)のあるサブシーケンス（部分列）である、なぜなら、\(n_1 \lt n_2\)を満たす各\(n_1, n_2 \in \mathbb{N}\)に対して、\(f \circ g^{-1} (n_1) \lt f \circ g^{-1} (n_2)\)、なぜなら、\(g^{-1} (n_1) \lt g^{-1} (n_2)\)、したがって、\(f \circ g^{-1} (n_1) \lt f \circ g^{-1} (n_2)\); 各\(n \in \mathbb{N}\)に対して、以下を満たすある\({J^`}_{n' + 1} \in J^`\)、つまり、\(n \le f ({J^`}_{n' + 1})\)、がある、そして、\(n \le f ({J^`}_{n' + 1}) = f \circ g^{-1} (n')\)。
\(\widetilde{s^`}\)は\(lim s^`\)へコンバージ（収束）する、なぜなら、\(0 \lt \epsilon\)を満たす各\(\epsilon \in \mathbb{R}\)に対して、以下を満たすある\(N \in \mathbb{N}\)、つまり、\(N \lt n\)を満たす各\(n \in \mathbb{N} \setminus \{0\}\)に対して、\(dist (lim s^`, s^` ({J^`}_n)) \lt \epsilon\)、がある、すると、各\(N \lt n\)に対して、\(dist (lim s^`, s^` \circ g^{-1} (n)) \lt \epsilon\)、なぜなら、\({J^`}_{N + 1} = g^{-1} (N) \lt g^{-1} (n)\)。
したがって、ステートメント（言明）Cが成立する。
ステップ5:
ステートメント（言明）Cを仮定しよう。
ステップ6:
\(s: J \to M\)を任意のものとしよう。
\(J\)がファイナイト（有限）である時は、あるコンバージェント（収束する）サブシーケンス（部分列）がある、なぜなら、\(s\)自体があるコンバージェント（収束する）サブシーケンス（部分列）である。
そうでないと仮定しよう。
順序維持バイジェクション（全単射）\(g: J \to \mathbb{N}, J_n \mapsto n - 1\)がある、それは、本当に順序維持である、なぜなら、各\(J_n \lt J_{n'}\)に対して、\(n \lt n'\)、したがって、\(n - 1 \lt n' - 1\); それは、本当に、あるバイジェクション（全単射）である、なぜなら、各\(J_n \neq J_{n'}\)に対して、\(n \neq n'\)、したがって、\(n - 1 \neq n' - 1\)、そして、各\(n \in \mathbb{N}\)に対して、\(J_{n + 1}\)は\(n\)へマップされる。
注意として、\(g^{-1}\)も順序維持である、なぜなら、各\(n \lt n'\)に対して、\(g^{-1} (n) = J_{n + 1} \lt J_{n' + 1} = g^{-1} (n')\)。
ステートメント（言明）Cによって、\(\widetilde{s}: \mathbb{N} \to M = s \circ g^{-1}\)のあるコンバージェント（収束する）サブシーケンス（部分列）\(\widetilde{s}^`: \mathbb{N} \to M\)がある、それが意味するのは、\(\widetilde{s}^` = \widetilde{s} \circ f = s \circ g^{-1} \circ f\)。
\(\widetilde{s}^`\)は\(s\)のあるサブシーケンス（部分列）である、なぜなら、\(n_1 \lt n_2\)を満たす各\(n_1, n_2 \in \mathbb{N}\)に対して、\(g^{-1} \circ f (n_1) \lt g^{-1} \circ f (n_2)\)、なぜなら、\(f (n_1) \lt f (n_2)\)、したがって、\(g^{-1} \circ f (n_1) \lt g^{-1} \circ f (n_2)\)、そして、各\(J_n \in J\)に対して、\(J_n = g^{-1} (n - 1)\)、そして、以下を満たすある\(n' \in \mathbb{N}\)、つまり、\(n - 1 \le f (n')\)、がある、すると、\(J_n = g^{-1} (n - 1) \le g^{-1} \circ f (n')\)。
したがって、\(\widetilde{s}^`\)は、\(s\)のあるコンバージェント（収束する）サブシーケンス（部分列）で\(J^`\)を特に\(\mathbb{N}\)として取ったものである。
したがって、ステートメント（言明）Aは成立する。
