リアルナンバー（実数）たちセット（集合）でカノニカル（正典）オーダリング（順序）を持つもののサブセット（部分集合）たちの包含するコンバージェント（収束する）シーケンス（列）に対して、包含するコンバージェンス（収束部分集合）のサプリマム（上限）はサブセット（部分集合）たちのサプリマム（上限）たちのシーケンス（列）のコンバージェンス（収束ポイント）であることの記述/証明
話題
About: メトリックスペース（計量付き空間）
この記事の目次
開始コンテキスト
- 読者は、セット（集合）のサブセット（部分集合）たちのシーケンス（列）の包含するコンバージェンス（収束部分集合）の定義を知っている。
- 読者は、パーシャリーオーダードセット（半順序集合）のサブセット（部分集合）のサプリマム（上限）の定義を知っている。
- 読者は、メトリックスペース（計量付き空間）上のシーケンス（列）のコンバージェンス（収束ポイント）の定義を知っている。
- 読者は、任意のパーシャリーオーダードセット（半順序集合）、任意のサブセット（部分集合）、当該サブセット（部分集合）の任意のサブセット（部分集合）に対して、もしも、当該サブセット（部分集合）のインフィマム（下限）および当該サブセット（部分集合）のサブセット（部分集合）のインフィマム（下限）が存在する場合、当該サブセット（部分集合）のインフィマム（下限）は当該サブセット（部分集合）のサブセット（部分集合）のインフィマム（下限）に等しいかそれより小さく、もしも、当該サブセット（部分集合）のサプリマム（上限）および当該サブセット（部分集合）のサブセット（部分集合）のサプリマム（上限）が存在する場合、当該サブセット（部分集合）のサプリマム（上限）は当該サブセット（部分集合）のサブセット（部分集合）のサプリマム（上限）に等しいかそれより大きいという命題を認めている。
- 読者は、任意のリニアリーオーダードセット（線形順序集合）および任意のサブセット（部分集合）に対して、当該セット（集合）の任意の要素は当該サブセット（部分集合）のサプリマム（上限）である、もしも、当該要素が当該サブセット（部分集合）の各要素に等しいかそれより大きく、当該要素より小さい当該セット（集合）の各要素に対して、より大きい当該サブセット（部分集合）のある要素がある場合、そしてその場合に限って、という命題を認めている。
ターゲットコンテキスト
- 読者は、リアルナンバー（実数）たちセット（集合）でカノニカル（正典）オーダリング（順序）を持つもののサブセット（部分集合）たちの任意の包含するコンバージェント（収束する）シーケンス（列）に対して、もしも、当該包含するコンバージェンス（収束部分集合）のサプリマム（上限）が存在しない場合、当該サブセット（部分集合）たちのサプリマム（上限）たちのシーケンス（列）のコンバージェンス（収束ポイント）は存在しない、そして、そうでない場合、当該包含するコンバージェンス（収束部分集合）のサプリマム（上限）は当該サブセット（部分集合）たちのサプリマム（上限）たちのシーケンス（列）のコンバージェンス（収束ポイント）であるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(J\): \(\subseteq \mathbb{N}\)で、以下を満たすもの、つまり、\(J \neq \emptyset\)
\(\mathbb{R}\): で、カノニカル（正典）オーダリング（順序）を持つもの
\(s\): \(\in \{\text{ 全てのシーケンス（列）たち }\}\)で、以下を満たすもの、つまり、\(Dom (s) = J\)および\(Ran (s) \subseteq Pow (\mathbb{R})\)および\(\exists lim_{ci} s\)
\(s'\): \(: J \to \mathbb{R}, j \mapsto Sup (s (j))\)、それは、存在しないかもしれない
//
ステートメント（言明）たち:
(
\(\lnot \exists Sup (lim_{ci} s)\)
\(\implies\)
\(\lnot \exists lim s'\)
)
\(\land\)
(
\(\exists Sup (lim_{ci} s)\)
\(\implies\)
\(\exists lim s' \land Sup (lim_{ci} s) = lim s'\)
)
//
2: 注
あるリアルナンバー（実数）たちセット（集合）でカノニカル（正典）オーダリング（順序）を持つもののサブセット（部分集合）たちの包含されるコンバージェント（収束する）シーケンス（列）に対する類似の命題は成立しない、一般に。
例えば、\(J = \mathbb{N}\)および\(s: J \to Pow (\mathbb{R}), n \mapsto (-1, 1) \cup \{2 - (1 / 2)^j \vert j \in \mathbb{N} \text{ で、以下を満たすもの、つまり、 } n \le j\}\)としよう。すると、\(lim_{ce} s = (-1, 1)\)、なぜなら、\((-1, 1) \subseteq (-1, 1) \cup \{2 - (1 / 2)^j \vert j \in \mathbb{N} \text{ で、以下を満たすもの、つまり、 } n \le j\}\)および\(2 - (1 / 2)^{j'} \notin \{2 - (1 / 2)^j \vert j \in \mathbb{N} \text{ で、以下を満たすもの、つまり、 } n \le j\}\)、各\(j' \lt n\)に対して。しかし、\(Sup (lim_{ce} s) = lim s'\)は成立しない、なぜなら、\(s' (n) = Sup (s (n)) = 2\)、各\(n\)に対して、したがって、\(s'\)は\(1 = Sup ((- 1, 1))\)に近づかない。
リアルナンバー（実数）たちセット（集合）でカノニカル（正典）オーダリング（順序）を持つもののサブセット（部分集合）たちの任意の包含するコンバージェント（収束する）シーケンス（列）に対して、もしも、当該包含するコンバージェンス（収束部分集合）のインフィマム（下限）が存在しない場合、当該サブセット（部分集合）たちのインフィマム（下限）たちのシーケンス（列）のコンバージェンス（収束ポイント）は存在しない、そして、そうでない場合、当該包含するコンバージェンス（収束部分集合）のインフィマム（下限）は当該サブセット（部分集合）たちのインフィマム（下限）たちのシーケンス（列）のコンバージェンス（収束ポイント）であるという命題と比較のこと。
したがって、リアルナンバー（実数）たちセット（集合）でカノニカル（正典）オーダリング（順序）を持つもののサブセット（部分集合）たちの任意の包含するコンバージェント（収束する）シーケンス（列）に対して、インフィマム（下限）版もサプリマム（上限）版も成立する、その一方で、あるリアルナンバー（実数）たちセット（集合）でカノニカル（正典）オーダリング（順序）を持つもののサブセット（部分集合）たちのある包含されるコンバージェント（収束する）シーケンス（列）に対して、インフィマム（下限）版もサプリマム（上限）版も成立しない。
3: 証明
全体戦略: ステップ1: \(J\)がファイナイト（有限）であるケースに対処し、それ以降はそうでないと仮定する; ステップ2: \(Sup (lim_{ci} s)\)は存在しないと仮定する; ステップ3: \(lim s'\)は存在しないことを見る; ステップ4: \(Sup (lim_{ci} s)\)は存在すると仮定する; ステップ5: \(Sup (lim_{ci} s) = lim s'\)であることを見る。
ステップ1:
\(\vert J \vert \in \mathbb{N} \setminus \{0\}\)であると仮定しよう。
\(lim_{ci} s = s (J_{\vert J \vert})\)。
\(Sup (lim_{ci} s) = Sup (s (J_{\vert J \vert}))\)が存在しない時、\(s'\)は存在しない、したがって、\(lim s'\)は存在しない。
\(Sup (lim_{ci} s) = Sup (s (J_{\vert J \vert}))\)が存在する時、各\(Sup (s (j))\)は存在する、なぜなら、\(s (j) \subseteq s (J_{\vert J \vert})\)、したがって、\(s'\)は存在する、そして、\(lim s' = Sup (s (J_{\vert J \vert}))\)は存在する、そして、\(Sup (lim_{ci} s) = Sup (s (J_{\vert J \vert})) = lim s'\)。
これ以降は、そうでないと仮定しよう。
ステップ2:
\(Sup (lim_{ci} s)\)は存在しないと仮定しよう。
ステップ3:
それが意味するのは、\(lim_{ci} s\)はアッパーバウンデッド（上方有界）でないということ。
それが意味するのは、各\(r' \in \mathbb{R}\)に対して、以下を満たすある\(r \in lim_{ci} s\)、つまり、\(r' \lt r\)、がある。
すると、以下を満たすある\(N \in \mathbb{N}\)、つまり、\(N \lt n\)を満たす各\(n \in \mathbb{N} \setminus \{0\}\)に対して、\(r \in s (J_n)\)、したがって、\(r' \lt r \le Sup (s (J_n))\)、もしも、\(Sup (s (J_n))\)が存在する場合も（そうでない場合、\(s'\)は存在しない、そして、当該主張は成立する）。
もしも、ある\(lim s' \in \mathbb{R}\)があったら、以下を満たすある\(N' \in \mathbb{N}\)、つまり、\(N' \lt n'\)を満たす各\(n' \in \mathbb{N} \setminus \{0\}\)に対して、\(\vert lim s' - Sup (s (J_{n'})) \vert \lt 1\)、があることになる、したがって、\(lim s' - 1 \lt Sup (s (J_{n'})) \lt lim s' + 1\)。
しかし、\(r' = lim s' + 1\)と取ると、各\(N, N' \lt n'\)に対して、\(lim s' + 1 \lt Sup (s (J_{n'}))\)、したがって、\(Sup (s (J_{n'})) \lt lim s' + 1 \lt Sup (s (J_{n'}))\)、矛盾。
したがって、\(lim s' \in \mathbb{R}\)はない。
ステップ4:
\(Sup (lim_{ci} s)\)は存在すると仮定しよう。
ステップ5:
それが意味するのは、\(lim_{ci} s\)はアッパーバウンデッド（上方有界）であること。
各\(Sup (s (j))\)は存在する、なぜなら、\(s (j) \subseteq lim_{ci} s\)。
したがって、\(s'\)は存在する。
\(Sup (s (j)) \le Sup (lim_{ci} s)\)、任意のパーシャリーオーダードセット（半順序集合）、任意のサブセット（部分集合）、当該サブセット（部分集合）の任意のサブセット（部分集合）に対して、もしも、当該サブセット（部分集合）のインフィマム（下限）および当該サブセット（部分集合）のサブセット（部分集合）のインフィマム（下限）が存在する場合、当該サブセット（部分集合）のインフィマム（下限）は当該サブセット（部分集合）のサブセット（部分集合）のインフィマム（下限）に等しいかそれより小さく、もしも、当該サブセット（部分集合）のサプリマム（上限）および当該サブセット（部分集合）のサブセット（部分集合）のサプリマム（上限）が存在する場合、当該サブセット（部分集合）のサプリマム（上限）は当該サブセット（部分集合）のサブセット（部分集合）のサプリマム（上限）に等しいかそれより大きいという命題によって。
\(\epsilon \in \mathbb{R}\)を、\(0 \lt \epsilon\)を満たす任意のものとしよう。
以下を満たすある\(r \in lim_{ci} s\)、つまり、\(Sup (lim_{ci} s) - \epsilon \lt r\)、がある、任意のリニアリーオーダードセット（線形順序集合）および任意のサブセット（部分集合）に対して、当該セット（集合）の任意の要素は当該サブセット（部分集合）のサプリマム（上限）である、もしも、当該要素が当該サブセット（部分集合）の各要素に等しいかそれより大きく、当該要素より小さい当該セット（集合）の各要素に対して、より大きい当該サブセット（部分集合）のある要素がある場合、そしてその場合に限って、という命題によって。
しかし、以下を満たすある\(N \in \mathbb{N}\)、つまり、\(n \lt N\)を満たす各\(n \in \mathbb{N} \setminus \{0\}\)に対して、\(r \in s (J_n)\)、がある、したがって、\(Sup (lim_{ci} s) - \epsilon \lt r \le Sup (s (J_n))\)。
したがって、\(s' (J_n) = Sup (s (J_n))\)であるから、\(Sup (lim_{ci} s) - \epsilon \lt s' (J_n) \le Sup (lim_{ci} s)\)、\(N \lt n\)を満たす各\(n \in \mathbb{N} \setminus \{0\}\)に対して、それが意味するのは、\(\vert s' (J_n) - Sup (lim_{ci} s) \vert \lt \epsilon\)。
したがって、\(lim s' = Sup (lim_{ci} s)\)。
