リアルナンバー（実数）たちセット（集合）でカノニカル（正典）オーダリング（順序）を持つもののサブセット（部分集合）たちの包含するコンバージェント（収束する）シーケンス（列）に対して、包含するコンバージェンス（収束部分集合）のインフィマム（下限）はサブセット（部分集合）たちのインフィマム（下限）たちのシーケンス（列）のコンバージェンス（収束ポイント）であることの記述/証明
話題
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 Inf (s (j))\)、それは、存在しないかもしれない
//
ステートメント（言明）たち:
(
\(\lnot \exists Inf (lim_{ci} s)\)
\(\implies\)
\(\lnot \exists lim s'\)
)
\(\land\)
(
\(\exists Inf (lim_{ci} s)\)
\(\implies\)
\(\exists lim s' \land Inf (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{ such that } n \le j\}\)および\(- 2 + (1 / 2)^{j'} \notin \{- 2 + (1 / 2)^j \vert j \in \mathbb{N} \text{ で、以下を満たすもの、つまり、 } n \le j\}\)、各\(j' \lt n\)に対して。しかし、\(Inf (lim_{ce} s) = lim s'\)は成立しない、なぜなら、\(s' (n) = Inf (s (n)) = - 2\)、各\(n\)に対して、したがって、\(s'\)は\(- 1 = Inf ((- 1, 1))\)に近づかない。
リアルナンバー（実数）たちセット（集合）でカノニカル（正典）オーダリング（順序）を持つもののサブセット（部分集合）たちの任意の包含するコンバージェント（収束する）シーケンス（列）に対して、もしも、当該包含するコンバージェンス（収束部分集合）のサプリマム（上限）が存在しない場合、当該サブセット（部分集合）たちのサプリマム（上限）たちのシーケンス（列）のコンバージェンス（収束ポイント）は存在しない、そして、そうでない場合、当該包含するコンバージェンス（収束部分集合）のサプリマム（上限）は当該サブセット（部分集合）たちのサプリマム（上限）たちのシーケンス（列）のコンバージェンス（収束ポイント）であるという命題と比較のこと。
したがって、リアルナンバー（実数）たちセット（集合）でカノニカル（正典）オーダリング（順序）を持つもののサブセット（部分集合）たちの任意の包含するコンバージェント（収束する）シーケンス（列）に対して、インフィマム（下限）版もサプリマム（上限）版も成立する、その一方で、あるリアルナンバー（実数）たちセット（集合）でカノニカル（正典）オーダリング（順序）を持つもののサブセット（部分集合）たちのある包含されるコンバージェント（収束する）シーケンス（列）に対して、インフィマム（下限）版もサプリマム（上限）版も成立しない。
3: 証明
全体戦略: ステップ1: \(J\)がファイナイト（有限）であるケースに対処し、それ以降はそうでないと仮定する; ステップ2: \(Inf (lim_{ci} s)\)は存在しないと仮定する; ステップ3: \(lim s'\)は存在しないことを見る; ステップ4: \(Inf (lim_{ci} s)\)は存在すると仮定する; ステップ5: \(Inf (lim_{ci} s) = lim s'\)であることを見る。
ステップ1:
\(\vert J \vert \in \mathbb{N} \setminus \{0\}\)であると仮定しよう。
\(lim_{ci} s = s (J_{\vert J \vert})\)。
\(Inf (lim_{ci} s) = Inf (s (J_{\vert J \vert}))\)が存在しない時、\(s'\)は存在しない、したがって、\(lim s'\)は存在しない。
\(Inf (lim_{ci} s) = Inf (s (J_{\vert J \vert}))\)が存在する時、各\(Inf (s (j))\)は存在する、なぜなら、\(s (j) \subseteq s (J_{\vert J \vert})\)、したがって、\(s'\)は存在する、そして、\(lim s' = Inf (s (J_{\vert J \vert}))\)は存在する、そして、\(Inf (lim_{ci} s) = Inf (s (J_{\vert J \vert})) = lim s'\)。
これ以降は、そうでないと仮定しよう。
ステップ2:
\(Inf (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)\)、したがって、\(Inf (s (J_n)) \le r \lt r'\)、もしも、\(Inf (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' - Inf (s (J_{n'})) \vert \lt 1\)、があることになる、したがって、\(lim s' - 1 \lt Inf (s (J_{n'})) \lt lim s' + 1\)。
しかし、\(r' = lim s' - 1\)と取ると、各\(N, N' \lt n'\)に対して、\(Inf (s (J_{n'})) \lt lim s' - 1\)、したがって、\(Inf (s (J_{n'})) \lt lim s' - 1 \lt Inf (s (J_{n'}))\)、矛盾。
したがって、\(lim s' \in \mathbb{R}\)はない。
ステップ4:
\(Inf (lim_{ci} s)\)は存在すると仮定しよう。
ステップ5:
それが意味するのは、\(lim_{ci} s\)はローワーバウンデッド（下方有界）であること。
各\(Inf (s (j))\)は存在する、なぜなら、\(s (j) \subseteq lim_{ci} s\)。
したがって、\(s'\)は存在する。
\(Inf (lim_{ci} s) \le Inf (s (j))\)、任意のパーシャリーオーダードセット（半順序集合）、任意のサブセット（部分集合）、当該サブセット（部分集合）の任意のサブセット（部分集合）に対して、もしも、当該サブセット（部分集合）のインフィマム（下限）および当該サブセット（部分集合）のサブセット（部分集合）のインフィマム（下限）が存在する場合、当該サブセット（部分集合）のインフィマム（下限）は当該サブセット（部分集合）のサブセット（部分集合）のインフィマム（下限）に等しいかそれより小さく、もしも、当該サブセット（部分集合）のサプリマム（上限）および当該サブセット（部分集合）のサブセット（部分集合）のサプリマム（上限）が存在する場合、当該サブセット（部分集合）のサプリマム（上限）は当該サブセット（部分集合）のサブセット（部分集合）のサプリマム（上限）に等しいかそれより大きいという命題によって。
\(\epsilon \in \mathbb{R}\)を、\(0 \lt \epsilon\)を満たす任意のものとしよう。
以下を満たすある\(r \in lim_{ci} s\)、つまり、\(r \lt Inf (lim_{ci} s) + \epsilon\)、がある、任意のリニアリーオーダードセット（線形順序集合）および任意のサブセット（部分集合）に対して、当該セット（集合）の任意の要素は当該サブセット（部分集合）のインフィマム（下限）である、もしも、当該要素が当該サブセット（部分集合）の各要素に等しいかそれより小さく、当該要素より大きい当該セット（集合）の各要素に対して、より小さい当該サブセット（部分集合）のある要素がある場合、そしてその場合に限って、という命題によって。
しかし、以下を満たすある\(N \in \mathbb{N}\)、つまり、\(n \lt N\)を満たす各\(n \in \mathbb{N} \setminus \{0\}\)に対して、\(r \in s (J_n)\)、がある、したがって、\(Inf (s (J_n)) \le r \lt Inf (lim_{ci} s) + \epsilon\)。
したがって、\(s' (J_n) = Inf (s (J_n))\)であるから、\(Inf (lim_{ci} s) \le s' (J_n) \lt Inf (lim_{ci} s) + \epsilon\)、\(N \lt n\)を満たす各\(n \in \mathbb{N} \setminus \{0\}\)に対して、それが意味するのは、\(\vert s' (J_n) - Inf (lim_{ci} s) \vert \lt \epsilon\)。
したがって、\(lim s' = Inf (lim_{ci} s)\)。
