\(1\)-ディメンショナル（次元）ユークリディアンメトリックスペース（計量付き空間）でカノニカル（正典）オーダリング（順序）を持つもの上のシーケンス（列）に対して、もしも、リミットスピアリア（上極限）が存在する場合、リミットスピアリア（上極限）へコンバージ（収束）するサブシーケンス（部分列）があることの記述/証明
話題
About: メトリックスペース（計量付き空間）
この記事の目次
開始コンテキスト
- 読者は、パーシャリーオーダードセット（半順序集合）上のシーケンス（列）のリミットスピアリア（上極限）の定義を知っている。
- 読者は、シーケンス（列）のサブシーケンス（部分列）の定義を知っている。
- 読者は、メトリックスペース（計量付き空間）上のシーケンス（列）のコンバージェンス（収束ポイント）の定義を知っている。
- 読者は、任意のリニアリーオーダードセット（線形順序集合）および任意のサブセット（部分集合）に対して、当該セット（集合）の任意の要素は当該サブセット（部分集合）のインフィマム（下限）である、もしも、当該要素が当該サブセット（部分集合）の各要素に等しいかそれより小さく、当該要素より大きい当該セット（集合）の各要素に対して、より小さい当該サブセット（部分集合）のある要素がある場合、そしてその場合に限って、という命題を認めている。
- 読者は、任意のリニアリーオーダードセット（線形順序集合）および任意のサブセット（部分集合）に対して、当該セット（集合）の任意の要素は当該サブセット（部分集合）のサプリマム（上限）である、もしも、当該要素が当該サブセット（部分集合）の各要素に等しいかそれより大きく、当該要素より小さい当該セット（集合）の各要素に対して、より大きい当該サブセット（部分集合）のある要素がある場合、そしてその場合に限って、という命題を認めている。
- 読者は、任意のパーシャリーオーダードセット（半順序集合）、任意のサブセット（部分集合）、当該サブセット（部分集合）の任意のサブセット（部分集合）に対して、もしも、当該サブセット（部分集合）のインフィマム（下限）および当該サブセット（部分集合）のサブセット（部分集合）のインフィマム（下限）が存在する場合、当該サブセット（部分集合）のインフィマム（下限）は当該サブセット（部分集合）のサブセット（部分集合）のインフィマム（下限）に等しいかそれより小さく、もしも、当該サブセット（部分集合）のサプリマム（上限）および当該サブセット（部分集合）のサブセット（部分集合）のサプリマム（上限）が存在する場合、当該サブセット（部分集合）のサプリマム（上限）は当該サブセット（部分集合）のサブセット（部分集合）のサプリマム（上限）に等しいかそれより大きいという命題を認めている。
ターゲットコンテキスト
- 読者は、\(1\)-ディメンショナル（次元）ユークリディアンメトリックスペース（計量付き空間）でカノニカル（正典）オーダリング（順序）を持つもの上の任意のシーケンス（列）に対して、もしも、リミットスピアリア（上極限）が存在する場合、リミットスピアリア（上極限）へコンバージ（収束）するあるサブシーケンス（部分列）があるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(J\): \(\subseteq \mathbb{N}\)で、以下を満たすもの、つまり、\(J \neq \emptyset\)
\(\mathbb{R}\): \(= \text{ 当該ユークリディアンメトリックスペース（計量付き空間） }\)で、カノニカル（正典）オーダリング（順序）\(\lt\)を持つもの
\(s\): \(\in \{\text{ 全てのシーケンス（列）たち }\}\)で、以下を満たすもの、つまり、\(Dom (s) = J\)および\(Ran (s) \subseteq \mathbb{R}\)
//
ステートメント（言明）たち:
\(\exists lim sup s\)
\(\implies\)
\(s^` \in \{s \text{ の全てのサブシーケンス（部分列）たち }\} (lim s^` = lim sup s)\)
//
2: 証明
全体戦略: ステップ1: \(J\)はファイナイト（有限）であるケースに対処し、それ以降は、そうでないと仮定する; ステップ2: \(l_1, l_2, ... \in \mathbb{N} \setminus \{0\}\)を、インダクティブ（帰納的）に、以下を満たすように選ぶ、つまり、\(l_1 \lt l_2 \lt ...\)および\(lim sup s - (1 / 2)^n \lt s (J_{l_n}) \lt lim sup s + (1 / 2)^n\)、各\(n \in \mathbb{N} \setminus \{0\}\)に対して; ステップ3: \(J^` = \mathbb{N} \setminus \{0\}\)および\(f: J^` \to J, n \mapsto J_{l_n}\)を取る。
ステップ1:
\(\vert J \vert = n \in \mathbb{N} \setminus \{0\}\)であると仮定しよう。
\(lim sup s = s (J_n)\)は不可避に存在する、そして、\(lim s = s (J_n)\)は存在する、そして、\(lim s = lim sup s\)。
したがって、\(s^` := s = s \circ f\)、\(f: J^` \to J = id\)を持って、としよう、すると、\(lim s^` = lim s = lim sup s\)。
これ以降は、そうでないと仮定しよう。
ステップ2:
\(l_1, l_2, ... \in \mathbb{N} \setminus \{0\}\)を、インダクティブ（帰納的）に、以下のとおり選ぼう。
\(n = 1\)としよう。
\(lim sup s = Inf (\{Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) \vert m \in \mathbb{N} \setminus \{0\}\})\)であるから、以下を満たすある\(m \in \mathbb{N} \setminus \{0\}\)、つまり、\(Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) \lt lim sup s + (1 / 2)^n\)、がある、任意のリニアリーオーダードセット（線形順序集合）および任意のサブセット（部分集合）に対して、当該セット（集合）の任意の要素は当該サブセット（部分集合）のインフィマム（下限）である、もしも、当該要素が当該サブセット（部分集合）の各要素に等しいかそれより小さく、当該要素より大きい当該セット（集合）の各要素に対して、より小さい当該サブセット（部分集合）のある要素がある場合、そしてその場合に限って、という命題によって: \(\mathbb{R}\)はリニアリーオーダード（線形順序付き）である。
\(lim sup s \le Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\})\)。
以下を満たすある\(l_n \in \mathbb{N} \setminus \{0\}\)、つまり、\(m \le l_n\)および\(Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) - (1 / 2)^n \lt s (J_{l_n})\)、がある、任意のリニアリーオーダードセット（線形順序集合）および任意のサブセット（部分集合）に対して、当該セット（集合）の任意の要素は当該サブセット（部分集合）のサプリマム（上限）である、もしも、当該要素が当該サブセット（部分集合）の各要素に等しいかそれより大きく、当該要素より小さい当該セット（集合）の各要素に対して、より大きい当該サブセット（部分集合）のある要素がある場合、そしてその場合に限って、という命題によって。
\(s (J_{l_n}) \le Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\})\)。
したがって、\(lim sup s - (1 / 2)^n \le Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) - (1 / 2)^n \lt s (J_{l_n}) \le Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) \lt lim sup s + (1 / 2)^n\)。
したがって、\(lim sup s - (1 / 2)^n \lt s (J_{l_n}) \lt lim sup s + (1 / 2)^n\)。
\(l_1, ..., l_{n' - 1}\)が以下を満たすように選ばれた、つまり、\(l_1 \lt ... \lt l_{n' - 1}\)および\(lim sup s - (1 / 2)^n \lt s (J_{l_n}) \lt lim sup s + (1 / 2)^n\)、各\(n \in \{1, ..., n' - 1\}\)に対して、と仮定しよう。
以下を満たすある\(m \in \mathbb{N} \setminus \{0\}\)、つまり、\(Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) \lt lim sup s + (1 / 2)^{n'}\)、がある、前と同様、しかし、\(m\)は、\(l_{n' - 1} \lt m\)を満たすように選ぶことができる、なぜなら、もしも、\(m \le l_{n' - 1}\)である場合、以下を満たす任意の\(m' \in \mathbb{N} \setminus \{0\}\)、つまり、\(l_{n' - 1} \lt m'\)、を取る、すると、\(Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m' \le n\}) \le Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) \lt lim sup s + (1 / 2)^{n'}\)、任意のパーシャリーオーダードセット（半順序集合）、任意のサブセット（部分集合）、当該サブセット（部分集合）の任意のサブセット（部分集合）に対して、もしも、当該サブセット（部分集合）のインフィマム（下限）および当該サブセット（部分集合）のサブセット（部分集合）のインフィマム（下限）が存在する場合、当該サブセット（部分集合）のインフィマム（下限）は当該サブセット（部分集合）のサブセット（部分集合）のインフィマム（下限）に等しいかそれより小さく、もしも、当該サブセット（部分集合）のサプリマム（上限）および当該サブセット（部分集合）のサブセット（部分集合）のサプリマム（上限）が存在する場合、当該サブセット（部分集合）のサプリマム（上限）は当該サブセット（部分集合）のサブセット（部分集合）のサプリマム（上限）に等しいかそれより大きいという命題によって: \(\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m' \le n\} \subseteq \{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}\)。
\(lim sup s \le Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\})\)。
以下を満たすある\(l_{n'} \in \mathbb{N} \setminus \{0\}\)、つまり、\(m \le l_{n'}\)および\(Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) - (1 / 2)^{n'} \lt s (J_{l_{n'}})\)、がある、前と同様、しかし、\(l_{n' - 1} \lt m \le l_{n'}\)。
\(s (J_{l_{n'}}) \le Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\})\)。
したがって、\(lim sup s - (1 / 2)^{n'} \le Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) - (1 / 2)^{n'} \lt s (J_{l_{n'}}) \le Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) \lt lim sup s + (1 / 2)^{n'}\)。
したがって、\(lim sup s - (1 / 2)^{n'} \lt s (J_{l_{n'}}) \lt lim sup s + (1 / 2)^{n'}\)。
したがって、\(l_1, l_2, ... \in \mathbb{N} \setminus \{0\}\)を、インダクティブ（帰納的）に、以下を満たすように、つまり、\(l_1 \lt l_2 \lt ...\)および\(lim sup s - (1 / 2)^n \lt s (J_{l_n}) \lt lim sup s + (1 / 2)^n\)、各\(n \in \mathbb{N} \setminus \{0\}\)に対して、選んだ。
ステップ3:
\(J^` = \mathbb{N} \setminus \{0\}\)を取ろう。
\(f: J^` \to J, n \mapsto J_{l_n}\)を取ろう。
すると、\(s^` = s \circ f: J^` \to \mathbb{R}\)は\(s\)のあるサブシーケンス（部分列）である、なぜなら、\(\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^`)))\): \(j = J_m\)および\(l_1 \lt l_2 \lt ...\)であるから、\(m \le l_n\)、ある\(n\)に対して、そして、\(j = J_m \le J_{l_n} = f (n)\)。
\(lim s^` = lim sup s\)、なぜなら、\(0 \lt \epsilon\)を満たす各\(\epsilon \in \mathbb{R}\)に対して、以下を満たすある\(N \in \mathbb{N} \setminus \{0\}\)、つまり、\((1 / 2)^N \lt \epsilon\)、がある、そして、\(N \lt n\)を満たす各\(n \in \mathbb{N} \setminus \{0\}\)に対して、\((1 / 2)^n \lt (1 / 2)^N \lt \epsilon\)、そして、\(lim sup s - \epsilon \lt lim sup s - (1 / 2)^n \lt s^` (n) = s \circ f (n) = s (J_{l_n}) \lt lim sup s + (1 / 2)^n \lt lim sup s + \epsilon\)、したがって、\(\vert s^` (n) - lim sup s \vert \lt \epsilon\)。
