リニアリーオーダードセット（線形順序集合）上のシーケンス（列）に対して、リミットスピアリア（上極限）は先行ファイナイト（有限）要素たちに依存しないことの記述/証明
話題
About: セット（集合）
この記事の目次
開始コンテキスト
ターゲットコンテキスト
- 読者は、任意のリニアリーオーダードセット（線形順序集合）上の任意のシーケンス（列）に対して、リミットスピアリア（上極限）は任意の先行ファイナイト（有限）要素たちに依存しないという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(J\): \(\subseteq \mathbb{N}\)で、以下を満たすもの、つまり、\(J \neq \emptyset\)
\(S\): \(\in \{\text{ 全てのリニアリーオーダードセット（線形順序集合）たち }\}\)で、任意のリニアオーダリング（線形順序）\(\lt\)を持つもの
\(s\): \(: J \to S\)
\(s'\): \(: J \to S\)
//
ステートメント（言明）たち:
\(\exists N \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } N \lt \vert J \vert (\forall n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } N \lt n (s (J_n) = s' (J_n)))\)
\(\implies\)
(
\(\lnot \exists lim sup s \iff \lnot \exists lim sup s'\)
\(\land\)
\((\exists lim sup s \lor \exists lim sup s') \implies lim sup s = lim sup s'\)
)
//
2: 証明
全体戦略: ステップ0: \(t_m := Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\})\)および\(t'_m := Sup (\{s' (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\})\)を定義し、\(t_{m'} \le t_m\)および\(t'_{m'} \le t'_m\)、各\(m \lt m'\)に対して、であることを見る; ステップ1: \(J\)がファイナイト（有限）であるケースに対処し、それ以降は、そうでないと仮定する; ステップ2: \(lim sup s\)は存在しないと仮定する; ステップ3: \(lim sup s'\)は存在しないことを見る; ステップ4: もしも、\(lim sup s'\)が存在しない場合、\(lim sup s\)は存在しないことを見る; ステップ5: 本命題を結論する。
ステップ0:
\(t_m := Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\})\)および\(t'_m := Sup (\{s' (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\})\)を定義しよう。
\(m, m' \in \mathbb{N} \setminus \{0\}\)を、\(m \lt m'\)を満たす任意のものとしよう。
もしも、\(t_{m'}\)が存在する場合、\(t_m\)は存在し\(t_{m'} \le t_m\)であることを見よう。
\(t_{m'}\)は存在すると仮定しよう。
\(t_m = Sup (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n \lt m'\} \cup \{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m' \le n\})\)。
\(Max (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たす、つまり、 } m \le n \lt m'\})\)は存在する、任意のリニアリーオーダードセット（線形順序集合）に対して、任意の非空ファイナイト（有限）サブセット（部分集合）はマキシマム（最大）およびミニマム（最小）を持つという命題によって。
\(t_{m'} \le Max (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n \lt m'\})\)である時、\(t_m = Max (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n \lt m'\})\)、なぜなら、各\(m \le n \lt m'\)に対して、\(s (J_n) \le Max (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n \lt m'\})\)、そして、各\(m' \le n\)に対して、\(s (J_n) \le t_{m'} \le Max (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n \lt m'\})\)、したがって、\(Max (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n \lt m'\}) \in Ub (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\})\)、そして、もしも、以下を満たすある\(u \in Ub (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\})\)、つまり、\(u \lt Max (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n \lt m'\})\)があったら、\(u \lt s (J_n)\)、ある\(m \le n \lt m'\)に対して、\(u\)が当該アッパーバウンド（上限）たちセット（集合）内にあったことに反する矛盾、したがって、\(Max (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n \lt m'\}) = Min (Ub (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\})) = t_m\)。
\(Max (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n \lt m'\}) \lt t_{m'}\)である時、\(t_m = t_{m'}\)、なぜなら、各\(m \le n \lt m'\)に対して、\(s (J_n) \le Max (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n \lt m'\}) \le t_{m'}\)、そして、各\(m' \le n\)に対して、\(s (J_n) \le t_{m'}\)、したがって、\(t_{m'} \in Ub (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\})\)、そして、もしも、以下を満たすある\(u \in Ub (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\})\)、つまり、\(u \lt t_{m'}\)、があったら、\(u \in Ub (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m' \le n\})\)、\(t_{m'}\)が当該アッパーバウンド（上限）たちセット（集合）のミニマム（最小）であったことに反する矛盾、したがって、\(t'_m = Min (Ub (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\})) = t_m\)。
したがって、\(t_m\)は存在する、いずれにせよ。
\(t_{m'} \le t_m\)であることを見よう。
上記に見られたとおり、\(t_{m'} \le Max (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n \lt m'\})\)である時、\(t_{m'} \le Max (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n \lt m'\}) = t_m\); \(Max (\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n \lt m'\}) \lt t_{m'}\)である時、\(t_{m'} = t_m \le t_m\)。
したがって、いずれにせよ、\(t_{m'} \le t_m\)。
余談として、もしも、\(t_m\)が存在する場合、\(t_{m'}\)は存在しないかもしれない、なぜなら、例えば、\(S = \mathbb{Q}\)に対して、\(t_{m'}\)が、\(\sqrt{2}\)へ漸近するあるシーケンス（列）として、存在しない時、\(t_m\)は、\(s (J_m) = 2\)によって存在し得る。
ステップ1:
\(\vert J \vert = n \in \mathbb{N} \setminus \{0\}\)である時、\(lim sup s = s (J_n)\)および\(lim sup s' = s' (J_n)\)は存在する、そして、\(s (J_n) = s' (J_n)\)であるから、\(lim sup s = lim sup s'\)。
これ以降、そうでないと仮定しよう。
ステップ2:
\(lim sup s\)は存在しないと仮定しよう、それが意味するのは、\(t_m\)がある\(m \in \mathbb{N} \setminus \{0\}\)に対して存在しない、または、\(t_m\)は各\(m \in \mathbb{N} \setminus \{0\}\)に対して存在するが\(Inf (\{t_m \vert m \in \mathbb{N} \setminus \{0\}\})\)は存在しない、こと。
ステップ3:
\(t_m\)がある\(m \in \mathbb{N} \setminus \{0\}\)に対して存在しないと仮定しよう。
\(N \lt m\)である時、\(\{s (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\} = \{s' (J_n) \vert n \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } m \le n\}\)、したがって、\(t'_m\)も存在しない、したがって、\(lim sup s'\)は存在しない。
\(m \le N\)であると仮定しよう。
ステップ0によって、もしも、\(t_{N + 1}\)が存在したら、\(t_m\)は存在することになる、したがって、\(t_{N + 1}\)は存在しない。
しかし、\(t'_{N + 1} = t_{N + 1}\)であるから、\(t'_{N + 1}\)は存在しない。
したがって、\(lim sup s'\)は存在しない。
\(t_m\)は各\(m \in \mathbb{N} \setminus \{0\}\)に対して存在するが\(Inf (\{t_m \vert m \in \mathbb{N} \setminus \{0\}\})\)は存在しないと仮定しよう。
\(Lb (\{t_m \vert m \in \mathbb{N} \setminus \{0\}\}) = Lb (\{t_m \vert m \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } N + 1 \le m\})\)であることを見よう。
各\(u \in Lb (\{t_m \vert m \in \mathbb{N} \setminus \{0\}\})\)に対して、\(u \le t_m\)、各\(m \in \mathbb{N} \setminus \{0\}\)に対して、したがって、特に、\(N + 1 \le m\)を満たす各\(m \in \mathbb{N} \setminus \{0\}\)に対して、それが意味するのは、\(u \in Lb (\{t_m \vert m \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } N + 1 \le m\})\)。
各\(u \in Lb (\{t_m \vert m \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } N + 1 \le m\})\)に対して、\(u \le t_m\)、\(N + 1 \le m\)を満たす各\(m \in \mathbb{N} \setminus \{0\}\)に対して、しかし、ステップ0によって、\(m \le N\)を満たす各\(m \in \mathbb{N} \setminus \{0\}\)に対して、\(u \le t_{N + 1} \le t_m\)、したがって、\(u \le t_m\)、各\(m \in \mathbb{N} \setminus \{0\}\)に対して、それが意味するのは、\(u \in Lb (\{t_m \vert m \in \mathbb{N} \setminus \{0\}\})\)。
したがって、\(Inf (\{t_m \vert m \in \mathbb{N} \setminus \{0\}\}) = Max (Lb (\{t_m \vert m \in \mathbb{N} \setminus \{0\}\}))\)は存在しないから、\(Max (Lb (\{t_m \vert m \in \mathbb{N} \setminus \{0\} \text{ such that } N + 1 \le m\}))\)は存在しない。
しかし、\(\{t_m \vert m \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } N + 1 \le m\} = \{t'_m \vert m \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } N + 1 \le m\}\)であるから、\(Inf (\{t'_m \vert m \in \mathbb{N} \setminus \{0\}\}) = Max (Lb (\{t'_m \vert m \in \mathbb{N} \setminus \{0\}\})) = Max (Lb (\{t'_m \vert m \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } N + 1 \le m\}))\)は存在しない。
したがって、\(lim sup s'\)は存在しない。
ステップ4:
対称性により、もしも、\(lim sup s'\)が存在しない場合、\(lim sup s\)は存在しない。
ステップ5:
\(lim sup s\)は存在すると仮定しよう。
ステップ3内で見られたとおり、\(Lb (\{t_m \vert m \in \mathbb{N} \setminus \{0\}\}) = Lb (\{t_m \vert m \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } N + 1 \le m\})\)。
したがって、\(lim sup s = Inf (\{t_m \vert m \in \mathbb{N} \setminus \{0\}\}) = Max (Lb (\{t_m \vert m \in \mathbb{N} \setminus \{0\}\})) = Max (Lb (\{t_m \vert m \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } N + 1 \le m\})) = Max (Lb (\{t'_m \vert m \in \mathbb{N} \setminus \{0\} \text{ で、以下を満たすもの、つまり、 } N + 1 \le m\})) = Max (Lb (\{t'_m \vert m \in \mathbb{N} \setminus \{0\}\})) = Inf (\{t'_m \vert m \in \mathbb{N} \setminus \{0\}\}) = lim sup s'\)。
\(lim sup s'\)が存在する時、対称性により、\(lim sup s = lim sup s'\)。
