リニアリーオーダードセット（線形順序集合）上の\(2\)個のシーケンス（列）たちで同一ドメイン（定義域）を持ちリミットスピアリア（上極限）たちを持つものたちに対して、もしも、後者シーケンス（列）が前者以上である場合、後者リミットスピアリア（上極限）は前者リミットスピアリア（上極限）以上であることの記述/証明
話題
About: セット（集合）
この記事の目次
開始コンテキスト
- 読者は、リニアリーオーダードセット（線形順序集合）の定義を知っている。
- 読者は、パーシャリーオーダードセット（半順序集合）上のシーケンス（列）のリミットスピアリア（上極限）の定義を知っている。
- 読者は、任意のパーシャリーオーダードセット（半順序集合）および任意のサブセット（部分集合）に対して、もしも、当該サブセット（部分集合）のミニマム（最小）が存在する場合、当該ミニマム（最小）はインフィマム（下限）であり、もしも、当該サブセット（部分集合）のマキシマム（最大）が存在する場合、当該マキシマム（最大）はサプリマム（上限）であるという命題を認めている。
- 読者は、任意のパーシャリーオーダードセット（半順序集合）、任意のサブセット（部分集合）、当該サブセット（部分集合）の任意のサブセット（部分集合）に対して、もしも、当該サブセット（部分集合）のインフィマム（下限）および当該サブセット（部分集合）のサブセット（部分集合）のインフィマム（下限）が存在する場合、当該サブセット（部分集合）のインフィマム（下限）は当該サブセット（部分集合）のサブセット（部分集合）のインフィマム（下限）に等しいかそれより小さく、もしも、当該サブセット（部分集合）のサプリマム（上限）および当該サブセット（部分集合）のサブセット（部分集合）のサプリマム（上限）が存在する場合、当該サブセット（部分集合）のサプリマム（上限）は当該サブセット（部分集合）のサブセット（部分集合）のサプリマム（上限）に等しいかそれより大きいという命題を認めている。
ターゲットコンテキスト
- 読者は、任意のリニアリーオーダードセット（線形順序集合）上の任意の\(2\)個のシーケンス（列）たちで任意の同一ドメイン（定義域）を持ち任意のリミットスピアリア（上極限）たちを持つものたちに対して、もしも、後者シーケンス（列）が前者シーケンス（列）以上である場合、後者リミットスピアリア（上極限）は前者リミットスピアリア（上極限）以上であるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(J\): \(\subseteq \mathbb{N}\)で、以下を満たすもの、つまり、\(J \neq \emptyset\)
\(S\): \(\in \{\text{ 全てのリニアリーオーダードセット（線形順序集合）たち }\}\)で、任意のリニアオーダリング（線形順序）\(\lt\)を持つもの
\(s_1\): \(: J \to S\)で、以下を満たすもの、つまり、\(\exists lim sup s_1\)
\(s_2\): \(: J \to S\)で、以下を満たすもの、つまり、\(\exists lim sup s_2\)
//
ステートメント（言明）たち:
\(\forall j \in J (s_1 (j) \le s_2 (j))\)
\(\implies\)
\(lim sup s_1 \le lim sup s_2\)
//
2: 証明
全体戦略: ステップ1: \(J\)がファイナイト（有限）であるケースに対処し、それ以降、そうでないと仮定する; ステップ2: \(Sup (\{s_1 (J_n) \vert m \le n\}) \le Sup (\{s_2 (J_n) \vert m \le n\})\)であることを見る; ステップ3: \(Inf (\{Sup (\{s_1 (J_n) \vert m \le n\})\}) \le Inf (\{Sup (\{s_2 (J_n) \vert m \le n\})\})\)であることを見る。
ステップ1:
\(\vert J \vert = n \in \mathbb{N} \setminus \{0\}\)である時、\(lim sup s_1 = s_1 (J_n) \le s_2 (J_n) = lim sup s_2\)。
これ以降、そうでないと仮定しよう。
ステップ2:
\(Ub (\{s_2 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) \subseteq Ub (\{s_1 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\})\)、なぜなら、各\(s \in Ub (\{s_2 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\})\)に対して、\(m \le n\)を満たす各\(n \in \mathbb{N} \setminus \{0\}\)に対して、\(s_2 (J_n) \le s\)、したがって、\(s_1 (J_n) \le s\)、したがって、\(s \in Ub (\{s_1 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\})\)。
したがって、\(Sup (\{s_1 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) = Min (Ub (\{s_1 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\})) \le Min (Ub (\{s_2 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\})) = Sup (\{s_2 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\})\)、任意のパーシャリーオーダードセット（半順序集合）および任意のサブセット（部分集合）に対して、もしも、当該サブセット（部分集合）のミニマム（最小）が存在する場合、当該ミニマム（最小）はインフィマム（下限）であり、もしも、当該サブセット（部分集合）のマキシマム（最大）が存在する場合、当該マキシマム（最大）はサプリマム（上限）であるという命題および任意のパーシャリーオーダードセット（半順序集合）、任意のサブセット（部分集合）、当該サブセット（部分集合）の任意のサブセット（部分集合）に対して、もしも、当該サブセット（部分集合）のインフィマム（下限）および当該サブセット（部分集合）のサブセット（部分集合）のインフィマム（下限）が存在する場合、当該サブセット（部分集合）のインフィマム（下限）は当該サブセット（部分集合）のサブセット（部分集合）のインフィマム（下限）に等しいかそれより小さく、もしも、当該サブセット（部分集合）のサプリマム（上限）および当該サブセット（部分集合）のサブセット（部分集合）のサプリマム（上限）が存在する場合、当該サブセット（部分集合）のサプリマム（上限）は当該サブセット（部分集合）のサブセット（部分集合）のサプリマム（上限）に等しいかそれより大きいという命題によって。
ステップ3:
\(Lb (\{Sup (\{s_1 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) \vert m \in \mathbb{N} \setminus \{0\}\}) \subseteq Lb (\{Sup (\{s_2 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) \vert m \in \mathbb{N} \setminus \{0\}\})\)、なぜなら、各\(s \in Lb (\{Sup (\{s_1 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) \vert m \in \mathbb{N} \setminus \{0\}\})\)に対して、\(s \le Sup (\{s_1 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\})\)、各\(m \in \mathbb{N} \setminus \{0\}\)に対して、したがって、\(s \le Sup (\{s_1 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) \le Sup (\{s_2 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\})\)、ステップ2によって、したがって、\(s \in Lb (\{Sup (\{s_2 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) \vert m \in \mathbb{N} \setminus \{0\}\})\)。
\(lim sup s_1 = Inf (\{Sup (\{s_1 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) \vert m \in \mathbb{N} \setminus \{0\}\}) = Max (Lb (\{Sup (\{s_1 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) \vert m \in \mathbb{N} \setminus \{0\}\})) \le Max (Lb (\{Sup (\{s_2 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) \vert m \in \mathbb{N} \setminus \{0\}\})) = Inf (\{Sup (\{s_2 (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) \vert m \in \mathbb{N} \setminus \{0\}\}) = lim sup s_2\)、任意のパーシャリーオーダードセット（半順序集合）および任意のサブセット（部分集合）に対して、もしも、当該サブセット（部分集合）のミニマム（最小）が存在する場合、当該ミニマム（最小）はインフィマム（下限）であり、もしも、当該サブセット（部分集合）のマキシマム（最大）が存在する場合、当該マキシマム（最大）はサプリマム（上限）であるという命題および任意のパーシャリーオーダードセット（半順序集合）、任意のサブセット（部分集合）、当該サブセット（部分集合）の任意のサブセット（部分集合）に対して、もしも、当該サブセット（部分集合）のインフィマム（下限）および当該サブセット（部分集合）のサブセット（部分集合）のインフィマム（下限）が存在する場合、当該サブセット（部分集合）のインフィマム（下限）は当該サブセット（部分集合）のサブセット（部分集合）のインフィマム（下限）に等しいかそれより小さく、もしも、当該サブセット（部分集合）のサプリマム（上限）および当該サブセット（部分集合）のサブセット（部分集合）のサプリマム（上限）が存在する場合、当該サブセット（部分集合）のサプリマム（上限）は当該サブセット（部分集合）のサブセット（部分集合）のサプリマム（上限）に等しいかそれより大きいという命題によって。
