パーシャリーオーダードリング（半順序環）上のシーケンス（列）に対して、もしも、リミットスピアリア（上極限）が存在する場合、（シーケンス（列）プラス要素）のリミットスピアリア（上極限）は存在し、(シーケンス（列）のリミットスピアリア（上極限））プラス要素に等しい、もしも、リミットインフェリア（下極限）が存在する場合、（シーケンス（列）プラス要素）のリミットインフェリア（下極限）は存在し、（シーケンス（列）のリミットインフェリア（下極限）プラス要素に等しいことの記述/証明
話題
About: リング（環）
この記事の目次
開始コンテキスト
- 読者は、パーシャリーオーダードリング（半順序環）の定義を知っている。
- 読者は、パーシャリーオーダードセット（半順序集合）上のシーケンス（列）のリミットスピアリア（上極限）の定義を知っている。
- 読者は、パーシャリーオーダードセット（半順序集合）上のシーケンス（列）のリミットインフェリア（下極限）を知っている。
- 読者は、任意のパーシャリーオーダードリング（半順序環）、任意のサブセット（部分集合）、任意の要素に対して、もしも、当該サブセット（部分集合）のサプリマム（上限）が存在する場合、（当該サブセット（部分集合）プラス当該要素）のサプリマム（上限）は存在し、（当該サブセット（部分集合）のサプリマム（上限））プラス当該要素に等しい、そして、もしも、当該サブセット（部分集合）のインフィマム（下限）が存在する場合、（当該サブセット（部分集合）プラス当該要素）のインフィマム（下限）は存在し、（当該サブセット（部分集合）のインフィマム（下限））プラス当該要素に等しいという命題を認めている。
ターゲットコンテキスト
- 読者は、任意のパーシャリーオーダードリング（半順序環）上の任意のシーケンス（列）に対して、もしも、当該シーケンス（列）のリミットスピアリア（上極限）が存在する場合、（当該シーケンス（列）プラス任意の要素）のリミットスピアリア（上極限）は存在し、(当該シーケンス（列）のリミットスピアリア（上極限））プラス当該要素に等しい、もしも、当該シーケンス（列）のリミットインフェリア（下極限）が存在する場合、（当該シーケンス（列）プラス任意の要素）のリミットインフェリア（下極限）は存在し、（当該シーケンス（列）のリミットインフェリア（下極限）プラス当該要素に等しいという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(J\): \(\subseteq \mathbb{N}\)で、以下を満たすもの、つまり、\(J \neq \emptyset\)
\(R\): \(\in \{\text{ 全てのパーシャリーオーダードリング（半順序環）たち }\}\)で、任意のパーシャルオーダリング（半順序）\(\lt\)を持つもの
\(s\): \(\in \{\text{ 全てのシーケンス（列）たち }\}\)で、以下を満たすもの、つまり、\(Dom (s) = J\)および\(Ran (s) \subseteq S\)
\(r\): \(\in R\)
//
ステートメント（言明）たち:
(
\(\exists lim sup s\)
\(\implies\)
\(\exists lim sup (s + r) \land lim sup (s + r) = (lim sup s) + r\)
)
\(\land\)
(
\(\exists lim inf s\)
\(\implies\)
\(\exists lim inf (s + r) \land lim inf (s + r) = (lim inf s) + r\)
)
//
2: 注
何らかの\(2\)個のシーケンス（列）たち\(s, s': J \to R\)に対して、"\(lim sup (s + s') = (lim sup s) + (lim sup s')\)"や"\(lim inf (s + s') = (lim inf s) + (lim inf s')\)"は一般に成立しない、ある同一ドメイン（定義域）を持つあるパーシャリーオーダードリング（半順序環）上の何らか\(2\)個のシーケンス（列）たちに対して、当該シーケンス（列）たちの合計のリミットスピアリア（上極限）は、必ずしも、当該シーケンス（列）たちのリミットスピアリア（上極限）たちの合計ではない、そして、当該シーケンス（列）たちの合計のリミットインフェリア（下極限）は、必ずしも、当該シーケンス（列）たちのリミットインフェリア（下極限）たちの合計ではないという命題によって。したがって、本命題に対して、\(r\)があるコンスタント要素である、あるシーケンス（列）ではなく、ことが決定的である。
3: 証明
全体戦略: 任意のパーシャリーオーダードリング（半順序環）、任意のサブセット（部分集合）、任意の要素に対して、もしも、当該サブセット（部分集合）のサプリマム（上限）が存在する場合、（当該サブセット（部分集合）プラス当該要素）のサプリマム（上限）は存在し、（当該サブセット（部分集合）のサプリマム（上限））プラス当該要素に等しい、そして、もしも、当該サブセット（部分集合）のインフィマム（下限）が存在する場合、（当該サブセット（部分集合）プラス当該要素）のインフィマム（下限）は存在し、（当該サブセット（部分集合）のインフィマム（下限））プラス当該要素に等しいという命題を適用する; ステップ1: \(J\)がファイナイト（有限）であるというケースに対処し、それ以降は、そうでないと仮定する; ステップ2: \(lim sup s\)は存在すると仮定する; ステップ3: \(lim sup (s + r) = (lim sup s) + r\)であることを見る; ステップ4: \(lim inf s\)は存在すると仮定する; ステップ5: \(lim inf (s + r) = (lim inf s) + r\)であることを見る。
ステップ1:
\(\vert J \vert = n \in \mathbb{N} \setminus \{0\}\)であると仮定しよう。
\(lim sup s\)は不可避に存在し、\(s (J_n)\)に等しい。
\(lim sup (s + r)\)は不可避に存在し、\(s (J_n) + r\)に等しい。
したがって、\(lim sup (s + r) = s (J_n) + r = (lim sup s) + r\)。
\(lim inf s\)は不可避に存在し、\(s (J_n)\)に等しい。
\(lim inf (s + r)\)は不可避に存在し、\(s (J_n) + r\)に等しい。
したがって、\(lim inf (s + r) = s (J_n) + r = (lim inf s) + r\)。
そうでないと仮定しよう、これ以降は。
ステップ2:
\(lim sup s\)は存在すると仮定しよう。
ステップ3:
\(lim sup s = Inf (\{Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ such that } m \le n\}) \vert m \in \mathbb{N} \setminus \{0\}\})\)、そして、それらサプリマム（上限）たちおよびインフィマム（下限）は存在する。
\(Sup (\{s (J_n) + r \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\})\)は存在し、\(= Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) + r\)、任意のパーシャリーオーダードリング（半順序環）、任意のサブセット（部分集合）、任意の要素に対して、もしも、当該サブセット（部分集合）のサプリマム（上限）が存在する場合、（当該サブセット（部分集合）プラス当該要素）のサプリマム（上限）は存在し、（当該サブセット（部分集合）のサプリマム（上限））プラス当該要素に等しい、そして、もしも、当該サブセット（部分集合）のインフィマム（下限）が存在する場合、（当該サブセット（部分集合）プラス当該要素）のインフィマム（下限）は存在し、（当該サブセット（部分集合）のインフィマム（下限））プラス当該要素に等しいという命題によって。
\(Inf (\{Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) + r \vert m \in \mathbb{N} \setminus \{0\}\})\)は存在し、\(= Inf (\{Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) \vert m \in \mathbb{N} \setminus \{0\}\}) + r\)、任意のパーシャリーオーダードリング（半順序環）、任意のサブセット（部分集合）、任意の要素に対して、もしも、当該サブセット（部分集合）のサプリマム（上限）が存在する場合、（当該サブセット（部分集合）プラス当該要素）のサプリマム（上限）は存在し、（当該サブセット（部分集合）のサプリマム（上限））プラス当該要素に等しい、そして、もしも、当該サブセット（部分集合）のインフィマム（下限）が存在する場合、（当該サブセット（部分集合）プラス当該要素）のインフィマム（下限）は存在し、（当該サブセット（部分集合）のインフィマム（下限））プラス当該要素に等しいという命題によって。
したがって、\(lim sup (s + r) = Inf (\{Sup (\{s (J_n) + r \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) \vert m \in \mathbb{N} \setminus \{0\}\}) = Inf (\{Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) + r \vert m \in \mathbb{N} \setminus \{0\}\}) = Inf (\{Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) \vert m \in \mathbb{N} \setminus \{0\}\}) + r = (lim inf s) + r\)、それは、存在する。
ステップ4:
\(lim inf s\)は存在すると仮定しよう。
ステップ5:
\(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\}\})\)、そして、それらインフィマム（下限）たちおよびサプリマム（上限）は存在する。
\(Inf (\{s (J_n) + r \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\})\)は存在し、\(= Inf (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) + r\)、任意のパーシャリーオーダードリング（半順序環）、任意のサブセット（部分集合）、任意の要素に対して、もしも、当該サブセット（部分集合）のサプリマム（上限）が存在する場合、（当該サブセット（部分集合）プラス当該要素）のサプリマム（上限）は存在し、（当該サブセット（部分集合）のサプリマム（上限））プラス当該要素に等しい、そして、もしも、当該サブセット（部分集合）のインフィマム（下限）が存在する場合、（当該サブセット（部分集合）プラス当該要素）のインフィマム（下限）は存在し、（当該サブセット（部分集合）のインフィマム（下限））プラス当該要素に等しいという命題によって。
\(Sup (\{Inf (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) + r \vert m \in \mathbb{N} \setminus \{0\}\})\)は存在し、\(= Sup (\{Inf (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) \vert m \in \mathbb{N} \setminus \{0\}\}) + r\)、任意のパーシャリーオーダードリング（半順序環）、任意のサブセット（部分集合）、任意の要素に対して、もしも、当該サブセット（部分集合）のサプリマム（上限）が存在する場合、（当該サブセット（部分集合）プラス当該要素）のサプリマム（上限）は存在し、（当該サブセット（部分集合）のサプリマム（上限））プラス当該要素に等しい、そして、もしも、当該サブセット（部分集合）のインフィマム（下限）が存在する場合、（当該サブセット（部分集合）プラス当該要素）のインフィマム（下限）は存在し、（当該サブセット（部分集合）のインフィマム（下限））プラス当該要素に等しいという命題によって。
したがって、\(lim inf (s + r) = Sup (\{Inf (\{s (J_n) + r \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) \vert m \in \mathbb{N} \setminus \{0\}\}) = Sup (\{Inf (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) + r \vert m \in \mathbb{N} \setminus \{0\}\}) = Sup (\{Inf (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}) \vert m \in \mathbb{N} \setminus \{0\}\}) + r = (lim inf s) + r\)、それは、存在する。
