\(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 inf s \land \exists lim sup s \land lim inf s = lim sup s\)
\(\implies\)
\(\exists lim s \land lim s = lim inf s = lim sup s\)
//
2: 証明
全体戦略: ステップ1: \(J\)はファイナイト（有限）であるケースに対処し、それ以降は、そうでないと仮定する; ステップ2: \(r := lim inf s = lim sup s\)とし、各\(\epsilon\)に対して、\(r - \epsilon \lt Inf (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) \le s (J_n)\)、ある\(m\)および各\(m \le n\)に対して、そして、\(s (J_n) \le Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m' \le n\}) \lt r + \epsilon\)、ある\(m'\)および各\(m' \le n\)に対して、であることを見、\(m, m' \lt N\)に対して、各\(N \lt n\)に対して、\(r - \epsilon \lt s (J_n) \lt r + \epsilon\)であることを見る。
ステップ1:
\(\vert J \vert = n \in \mathbb{N} - \setminus \{0\}\)であると仮定しよう。
\(lim inf s = s (J_n)\)および\(lim sup s = s (J_n)\)は、不可避に存在する、そして、\(lim s = s (J_n)\)は存在する、そして、\(lim s = lim inf s = lims sup s\)。
そうでないと仮定しよう。
ステップ2:
\(r := lim inf s = lim sup s\)としよう。
\(\epsilon \in \mathbb{R}\)を、\(0 \lt \epsilon\)を満たす任意のものとしよう。
\(lim inf s = Sup (\{Inf (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) \vert m \in \mathbb{N} \setminus \{0\}\})\)であるから、以下を満たすある\(m \in \{N\} \setminus \{0\}\)、つまり、\(r - \epsilon \lt Inf (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\})\)、がある、任意のリニアリーオーダードセット（線形順序集合）および任意のサブセット（部分集合）に対して、当該セット（集合）の任意の要素は当該サブセット（部分集合）のサプリマム（上限）である、もしも、当該要素が当該サブセット（部分集合）の各要素に等しいかそれより大きく、当該要素より小さい当該セット（集合）の各要素に対して、より大きい当該サブセット（部分集合）のある要素がある場合、そしてその場合に限って、という命題によって。
\(\le s (J_n)\)、\(m \le n\)を満たす各\(n \in \mathbb{N} \setminus \{0\}\)に対して。
\(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 \{N\} \setminus \{0\}\)、つまり、\(Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m' \le n\}) \lt r + \epsilon\)、がある、任意のリニアリーオーダードセット（線形順序集合）および任意のサブセット（部分集合）に対して、当該セット（集合）の任意の要素は当該サブセット（部分集合）のインフィマム（下限）である、もしも、当該要素が当該サブセット（部分集合）の各要素に等しいかそれより小さく、当該要素より大きい当該セット（集合）の各要素に対して、より小さい当該サブセット（部分集合）のある要素がある場合、そしてその場合に限って、という命題によって。
\(s (J_n) \le Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m' \le n\}) \lt r + \epsilon\)、\(m' \le n\).を満たす各\(n \in \mathbb{N} \setminus \{0\}\)に対して。
\(N \in \mathbb{N} \setminus \{0\}\)を、\(m, m' \lt N\)を満たす任意のものとしよう。
\(N \lt n\)を満たす各\(n \in \mathbb{N} \setminus \{0\}\)に対して、\(m, m' \lt n\)、したがって、\(r - \epsilon \lt s (J_n) \lt r + \epsilon\)、それが意味するのは、\(dist (r, s (J_n)) \lt \epsilon\)。
したがって、\(lim s = r = lim inf s = lim sup s\)。
