リアルナンバー（実数）たちセット（集合）でカノニカル（正典）オーダリング（順序）を持つもの上のシーケンス（列）に対して、もしも、リミットスピアリア（上極限）およびリミットスピアリア（上極限）が存在する場合、リミットスピアリア（上極限）はリミットスピアリア（上極限）以下であることの記述/証明
話題
About: セット（集合）
この記事の目次
開始コンテキスト
- 読者は、パーシャリーオーダードセット（半順序集合）上のシーケンス（列）のリミットインフェリア（下極限）の定義を知っている。
- 読者は、パーシャリーオーダードセット（半順序集合）上のシーケンス（列）のリミットスピアリア（上極限）を知っている。
- 読者は、任意のパーシャリーオーダードセット（半順序集合）、任意のサブセット（部分集合）、当該サブセット（部分集合）の任意のサブセット（部分集合）に対して、もしも、当該サブセット（部分集合）のインフィマム（下限）および当該サブセット（部分集合）のサブセット（部分集合）のインフィマム（下限）が存在する場合、当該サブセット（部分集合）のインフィマム（下限）は当該サブセット（部分集合）のサブセット（部分集合）のインフィマム（下限）に等しいかそれより小さく、もしも、当該サブセット（部分集合）のサプリマム（上限）および当該サブセット（部分集合）のサブセット（部分集合）のサプリマム（上限）が存在する場合、当該サブセット（部分集合）のサプリマム（上限）は当該サブセット（部分集合）のサブセット（部分集合）のサプリマム（上限）に等しいかそれより大きいという命題を認めている。
- 読者は、リアルナンバー（実数）たちセット（集合）上の任意の同一ドメイン（定義域）を持つ任意の非減少シーケンス（列）および任意の非増加シーケンス（列）で第1シーケンス（列）が第2シーケンス（列）以下であるものたちに対して、第1シーケンス（列）の各要素は第2シーケンス（列）の任意の要素以下であり、第1シーケンス（列）のサプリマム（上限）は第2シーケンス（列）のインフィマム（下限）以下であるという命題を認めている。
- 読者は、任意のパーシャリーオーダードセット（半順序集合）および任意の非空サブセット（部分集合）に対して、もしも、当該サブセット（部分集合）のインフィマム（下限）およびサプリマム（上限）が存在する場合、インフィマム（下限）はサプリマム（上限）以下であるという命題を認めている。
ターゲットコンテキスト
- 読者は、リアルナンバー（実数）たちセット（集合）でカノニカル（正典）オーダリング（順序）を持つもの上の任意のシーケンス（列）に対して、もしも、リミットスピアリア（上極限）およびリミットスピアリア（上極限）が存在する場合、リミットスピアリア（上極限）はリミットスピアリア（上極限）以下であるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(J\): \(\subseteq \mathbb{N}\)で、以下を満たすもの、つまり、\(J \neq \emptyset\)
\(\mathbb{R}\): で、カノニカル（正典）オーダリング（順序）\(\lt\)を持つもの
\(s\): \(\in \{\text{ 全てのシーケンス（列）たち }\}\)で、以下を満たすもの、つまり、\(Dom (s) = J\)および\(Ran (s) \subseteq \mathbb{R}\)
//
ステートメント（言明）たち:
\(\exists lim inf s \land \exists lim sup s\)
\(\implies\)
\(lim inf s \le lim sup s\)
//
2: 証明
全体戦略: ステップ1: \(J\)がファイナイト（有限）であるケースに対処し、それ以降は、そうでないと仮定する; ステップ2: リアルナンバー（実数）たちセット（集合）上の任意の同一ドメイン（定義域）を持つ任意の非減少シーケンス（列）および任意の非増加シーケンス（列）で第1シーケンス（列）が第2シーケンス（列）以下であるものたちに対して、第1シーケンス（列）の各要素は第2シーケンス（列）の任意の要素以下であり、第1シーケンス（列）のサプリマム（上限）は第2シーケンス（列）のインフィマム（下限）以下であるという命題を適用する。
ステップ1:
\(\vert J \vert = n \in \mathbb{N} \setminus \{0\}\)であると仮定しよう。
\(lim inf s = s (J_n) = lim sup s\)。
したがって、\(lim inf s \le lim sup s\)。
これ以降は、そうでないと仮定しよう。
ステップ2:
\(Inf (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\})\)は、非減少である、\(m\)に関して、そして、\(Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\})\)は、非増加である、\(m\)に関して、任意のパーシャリーオーダードセット（半順序集合）、任意のサブセット（部分集合）、当該サブセット（部分集合）の任意のサブセット（部分集合）に対して、もしも、当該サブセット（部分集合）のインフィマム（下限）および当該サブセット（部分集合）のサブセット（部分集合）のインフィマム（下限）が存在する場合、当該サブセット（部分集合）のインフィマム（下限）は当該サブセット（部分集合）のサブセット（部分集合）のインフィマム（下限）に等しいかそれより小さく、もしも、当該サブセット（部分集合）のサプリマム（上限）および当該サブセット（部分集合）のサブセット（部分集合）のサプリマム（上限）が存在する場合、当該サブセット（部分集合）のサプリマム（上限）は当該サブセット（部分集合）のサブセット（部分集合）のサプリマム（上限）に等しいかそれより大きいという命題によって。
\(Inf (\{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\})\)、任意のパーシャリーオーダードセット（半順序集合）および任意の非空サブセット（部分集合）に対して、もしも、当該サブセット（部分集合）のインフィマム（下限）およびサプリマム（上限）が存在する場合、インフィマム（下限）はサプリマム（上限）以下であるという命題によって。
\(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\}\}) \le Inf (\{Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) \vert m \in \mathbb{N} \setminus \{0\}\}) = lim sup s\)、リアルナンバー（実数）たちセット（集合）上の任意の同一ドメイン（定義域）を持つ任意の非減少シーケンス（列）および任意の非増加シーケンス（列）で第1シーケンス（列）が第2シーケンス（列）以下であるものたちに対して、第1シーケンス（列）の各要素は第2シーケンス（列）の任意の要素以下であり、第1シーケンス（列）のサプリマム（上限）は第2シーケンス（列）のインフィマム（下限）以下であるという命題によって。
