ダイレクテッド（有向）インデックスセット（集合）によるネットはユニバーサルサブネットを持つことの記述/証明
話題
About: トポロジカルスペース（空間）
この記事の目次
開始コンテキスト
- 読者は、ダイレクテッド（有向）インデックスセット（集合）によるネットのサブネットの定義を知っている。
- 読者は、ダイレクテッド（有向）インデックスセット（集合）によるユニバーサルネットの定義を知っている。
- 読者は、ダイレクテッド（有向）インデックスセット（集合）によるネットでフリークエント（頻繁）にサブセット（部分集合）内にあるものを知っている。
- 読者は、ゾーンの補助定理を認めている。
ターゲットコンテキスト
- 読者は、任意のダイレクテッド（有向）インデックスセット（集合）による任意のネットはあるユニバーサルサブネットを持つという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(D_2\): \(\in \{\text{ 全てのダイレクテッドセット（有向集合）たち }\}\)
\(T\): \(\in \{\text{ 全てのトポロジカルスペース（空間）たち }\}\)
\(f_2\): \(: D_2 \to T\)
//
ステートメント（言明）たち:
\(\exists D_1 \in \{\text{ 全てのダイレクテッドセット（有向集合）たち }\}, \exists f_1 : D_1 \to D_2 \in \{\text{ 全てのファイナルマップ（写像）たち }\} (f_2 \circ f_1 \in \{\text{ 全てのユニバーサルネットたち }\})\)
//
2: 証明
全体戦略: ステップ1: \(S' := \{S \subseteq Pow (T) \vert \forall s \in S (f_2 \in \{\text{ 全てのネットたちでフリークエント（頻繁）に } s \text{ 内にあるものたち }\}) \land \forall s_1, s_2 \in S (s_1 \cap s_2 \in S))\}\)で、以下を満たすリレーション（関係）、つまり、\(s'_1 \le s'_2\)、もしも、\(s'_1 \subseteq s'_2\)である場合、そしてその場合に限って、を持つものを定義する; ステップ2: あるマキシマル（極大）\(\widetilde{S} \in S'\)を取る、ゾーンの補助定理によって; ステップ3: \(D_1 := \{(\widetilde{s}, d_2) \in \widetilde{S} \times D_2 \vert f_2 (d_2) \in \widetilde{s}\}\)で、以下を満たすリレーション（関係）、つまり、\((\widetilde{s}_1, d_{2, 1}) \le (\widetilde{s}_2, d_{2, 2})\)、もしも、\(\widetilde{s}_2 \subseteq \widetilde{s}_1\)および\(d_{2, 1} \le d_{2, 2}\)である場合、そしてその場合に限って、を持つものを定義し、\(f_1: (\widetilde{s}, d_2) \mapsto d_2\)を定義する; ステップ4: \(f_2 \circ f_1\)はあるユニバーサルサブネットであることを見る。
ステップ1:
\(S' := \{S \subseteq Pow (T) \vert \forall s \in S (f_2 \in \{\text{ 全てのネットたちでフリークエント（頻繁）に } s \text{ 内にあるものたち }\}) \land \forall s_1, s_2 \in S (s_1 \cap s_2 \in S))\}\)を定義しよう、それは、本当にあるセット（集合）である、サブセット（部分集合）公理によって: \(S \subseteq Pow (T)\)は\(S \in Pow (Pow (T))\)に等しく、\(S\)の述語はある妥当なフォーミュラである。
\(S'\)は空でない、なぜなら、少なくとも、\(\{T\} \in S'\)。
\(S'\)上に、以下を満たすリレーション（関係）、つまり、各\(s'_1, s'_2 \in S'\)に対して、\(s'_1 \le s'_2\)、もしも、\(s'_1 \subseteq s'_2\)である場合、そしてその場合に限って、を定義しよう。
ステップ2:
\(S'\)の任意のチェーン（\(S'\)の以下を満たす任意の非空サブセット（部分集合）、つまり、当該サブセット（部分集合）の任意の2個の要素たちに対して、当該要素たちの1つは他方要素内に包含されている、を意味する）\(C = \{S_j \vert j \in J\} \subseteq S'\)に対して、\(\cup C \in S'\)、なぜなら、各\(s \in \cup C\)に対して、\(s \in S_j\)、ある\(S_j \in S'\)に対して、したがって、\(f_2\)はフリークエント（頻繁）に\(s\)内にある、そして、各\(s_1, s_2 \in \cup C\)に対して、\(s_1 \in S_j\)および\(s_2 \in S_l\)、しかし、\(S_j \subseteq S_l\)または\(S_l \subseteq S_j\)であるから、\(s_1, s_2 \in S_l\)または\(s_1, s_2 \in S_j\)、したがって、\(s_1 \cap s_2 \in S_l \subseteq \cup C\)または\(s_1 \cap s_2 \in S_j \subseteq \cup C\)。
したがって、ゾーンの補助定理によって、あるマキシマル（極大）要素\(\widetilde{S} \in S'\)がある。
注意として、\(T \in \widetilde{S}\)である、なぜなら、そうでなければ、\(\widetilde{S} \cup \{T\} \in S'\)、なぜなら、各\(s \in \widetilde{S} \cup \{T\}\)に対して、\(s \in \widetilde{S}\)または\(s = T\)、そして、\(s \in \widetilde{S}\)である時、\(f_2\)はフリークエント（頻繁）に\(s\)内にあることになり、\(s = T\)である時、\(f_2\)はフリークエント（頻繁）に\(T\)内にあることになり、そして、各\(s_1, s_2 \in \widetilde{S} \cup \{T\}\)に対して、\(s_1 \neq T\)および\(s_2 \neq T\)である時、\(s_1 \cap s_2 \in \widetilde{S} \subseteq \widetilde{S} \cup \{T\}\)、\(s_1 = T\)および\(s_2 \neq T\)である時、\(s_1 \cap s_2 = s_2 \in \widetilde{S} \subseteq \widetilde{S} \cup \{T\}\)、\(s_1 \neq T\)および\(s_2 = T\)である時、\(s_1 \cap s_2 = s_1 \in \widetilde{S} \subseteq \widetilde{S} \cup \{T\}\)、\(s_1 = T\)および\(s_2 = T\)である時、\(s_1 \cap s_2 = T \in \widetilde{S} \cup \{T\}\)、\(\widetilde{S}\)がマキシマル（極大）であることに反する矛盾。
ステップ3:
\(D_1 := \{(\widetilde{s}, d_2) \in \widetilde{S} \times D_2 \vert f_2 (d_2) \in \widetilde{s}\}\)を定義しよう。
注意として、各\(\widetilde{s} \in \widetilde{S}\)は\(D_1\)内に現われる、なぜなら、\(\widetilde{S} \in S'\)、それが意味するのは、以下を満たすある\({d_2}'\)、つまり、\(f_2 ({d_2}') \in \widetilde{s}\)、があること、したがって、\((\widetilde{s}, {d_2}') \in D_1\)。
\(D_1\)上に、以下を満たすリレーション（関係）、つまり、各\((\widetilde{s}_1, d_{2, 1}), (\widetilde{s}_2, d_{2, 2}) \in D_1\)に対して、\((\widetilde{s}_1, d_{2, 1}) \le ((\widetilde{s}_2, d_{2, 2})\)、もしも、\(\widetilde{s}_2 \subseteq \widetilde{s}_1\)および\(d_{2, 1} \le d_{2, 2}\)である場合、そしてその場合に限って、を定義しよう。
\(D_1\)はあるダイレクテッドセット（有向集合）である、なぜなら、1) \((\widetilde{s}, d_2) \leq (\widetilde{s}, d_2)\)、各\((\widetilde{s}, d_2) \in D_1\)に対して; 2) もしも、\((\widetilde{s}_1, d_{2, 1}) \leq (\widetilde{s}_2, d_{2, 2})\)および\((\widetilde{s}_2, d_{2, 2}) \leq (\widetilde{s}_3, d_{2, 3})\)である場合、\((\widetilde{s}_1, d_{2, 1}) \leq (\widetilde{s}_3, d_{2, 3})\)、なぜなら、\(\widetilde{s}_3 \subseteq \widetilde{s}_2 \subseteq \widetilde{s}_1\)および\(d_{2, 1} \le d_{2, 2} \le d_{2, 3}\); 3) 各ペア\((\widetilde{s}_1, d_{2, 1}), (\widetilde{s}_2, d_{2, 2}) \in D_1\)に対して、\(\widetilde{s}_3 := \widetilde{s}_1 \cap \widetilde{s}_2 \in \widetilde{S}\)および以下を満たす、ある\(d_{2, 4} \in D_2\)、つまり、\(d_{2, 1}, d_{2, 2} \le d_{2, 4}\)、およびある\(d_{2, 3} \in D_1\)、つまり、\(d_{2, 4} \le d_{2, 3}\)および\(f_2 (d_{2, 3}) \in \widetilde{s}_3\)を取る、すると、\((\widetilde{s}_3, d_{2, 3}) \in D_1\)および\((\widetilde{s}_1, d_{2, 1}), (\widetilde{s}_2, d_{2, 2}) \le (\widetilde{s}_3, d_{2, 3})\)。
\(f_1: (\widetilde{s}, d_2) \mapsto d_2\)を定義しよう。
\(f_1\)はファイナルである、なぜなら、各\(d_2 \in D_2\)に対して、以下を満たす任意の\(\widetilde{s} \in \widetilde{S}\)およびある\({d_2}' \in D_2\)、つまり、\(d_2 \le {d_2}'\)および\(f_2 ({d_2}') \in \widetilde{s}\)、を取る、すると、\((\widetilde{s}, {d_2}') \in D_1\)、そして、以下を満たす各\((\widetilde{s}', {d_2}'') \in D_1\)、つまり、\((\widetilde{s}, {d_2}') \le (\widetilde{s}', {d_2}'')\)、に対して、\(d_2 \le f_1 ((\widetilde{s}', {d_2}'')) = {d_2}''\)、なぜなら、\(d_2 \le {d_2}' \le {d_2}''\)。
したがって、\(f_2 \circ f_1\)はあるサブネットである。
ステップ4:
\(f_2 \circ f_1\)はあるユニバーサルサブネットであることを見よう。
\(S \subseteq T\)を任意のものとしよう。
もしも、\(f_2 \circ f_1\)はイベンチュアル（最終的）に\(T \setminus S\)内にある場合、\(f_2 \circ f_1\)がユニバーサルであるための条件たちは\(S\)に対して満たされている。
そうでないと仮定しよう。
それが含意するのは、以下を満たす\(d_1 \in D_1\)、つまり、\(d_1 \le {d_1}'\)を満たす各\({d_1}' \in D_1\)に対して、\(f_2 \circ f_1 ({d_1}') \in T \setminus S\)、は無いこと、それが含意するのは、各\(d_1 \in D_1\)に対して、以下を満たすある\({d_1}' \in D_1\)、つまり、\(d_1 \le {d_1}'\)および\(f_2 \circ f_1 ({d_1}') \notin T \setminus S\)、があること、それが含意するのは、\(f_2 \circ f_1 ({d_1}') \in S\)、それが意味するのは、\(f_2 \circ f_1\)はフリークエント（頻繁）に\(S\)内にあること。
\(\widetilde{s} \in \widetilde{S}\)を任意のものとしよう。
\(d_2 \in D_2\)を任意のものとしよう。
以下を満たすある\((\widetilde{s}, {d_2}') \in D_1\)、つまり、\(d_2 \le {d_2}'\)、がある。
以下を満たすある\((\widetilde{s}', {d_2}'') \in D_1\)、つまり、\((\widetilde{s}, {d_2}') \le (\widetilde{s}', {d_2}'')\)および\(f_2 \circ f_1 ((\widetilde{s}', {d_2}'')) = f_2 ({d_2}'') \in S\)、がある、なぜなら、\(f_2 \circ f_1\)はフリークエント（頻繁）に\(S\)内にある。
\(f_2 ({d_2}'') \in \widetilde{s}' \cap S \subseteq \widetilde{s} \cap S\)、それが意味するのは、\(f_2\)はフリークエント（頻繁）に\(\widetilde{s} \cap S\)内にあること: \(d_2 \le {d_2}' \le {d_2}''\)。
\(\widetilde{S} \cup \{\widetilde{s} \cap S \vert \widetilde{s} \in \widetilde{S}\}\)のことを考えよう。
\(\widetilde{S} \cup \{\widetilde{s} \cap S \vert \widetilde{s} \in \widetilde{S}\} \in S'\)、なぜなら、各\(\widetilde{s} \cap S\)に対して、\(f_2\)はフリークエント（頻繁）に\(\widetilde{s} \cap S\)内にある、そして、各\(s_1, s_2 \in \widetilde{S} \cup \{\widetilde{s} \cap S \vert \widetilde{s} \in \widetilde{S}\}\)に対して、\(s_1 \in \widetilde{S}\)および\(s_2 \in \widetilde{S}\)である時、\(s_1 \cap s_2 \in \widetilde{S} \subseteq \widetilde{S} \cup \{\widetilde{s} \cap S \vert \widetilde{s} \in \widetilde{S}\}\)、\(s_1 = \widetilde{s} \cap S\)および\(s_2 \in \widetilde{S}\)である時、\(s_1 \cap s_2 = \widetilde{s} \cap S \cap s_2 = (\widetilde{s} \cap s_2) \cap S \in \widetilde{S} \cup \{\widetilde{s} \cap S \vert \widetilde{s} \in \widetilde{S}\}\)、\(s_1 \in \widetilde{S}\)および\(s_2 = \widetilde{s} \cap S\)である時、\(s_1 \cap s_2 = s_1 \cap \widetilde{s} \cap S = (s_1 \cap \widetilde{s}) \cap S \in \widetilde{S} \cup \{\widetilde{s} \cap S \vert \widetilde{s} \in \widetilde{S}\}\)、\(s_1 = \widetilde{s}' \cap S\)および\(s_2 = \widetilde{s} \cap S\)である時、\(s_1 \cap s_2 = \widetilde{s} \cap S \cap \widetilde{s}' \cap S = (\widetilde{s} \cap \widetilde{s}') \cap S \in \widetilde{S} \cup \{\widetilde{s} \cap S \vert \widetilde{s} \in \widetilde{S}\}\)。
しかし、\(\widetilde{S}\)はマキシマル（極大）であるから、\(\widetilde{S} = \widetilde{S} \cup \{\widetilde{s} \cap S \vert \widetilde{s} \in \widetilde{S}\}\)。
特に、\(T \cap S = S \in \widetilde{S}\): \(T \in \widetilde{S}\)。
もしも、\(f_2 \circ f_1\)がフリークエント（頻繁）に\(T \setminus S\)内にあったら、\(T \setminus S \in \widetilde{S}\)、なぜなら、\(S \in \widetilde{S}\)に対するロジックは、\(S\)が、その内に\(f_2 \circ f_1\)がフリークエント（頻繁）にあるあるサブセット（部分集合）であったという仮定のみに基づいており、\(T \setminus S\)はそうしたあるサブセット（部分集合）であることになる。すると、\(S \cap (T \setminus S) = \emptyset \in \widetilde{S}\)、矛盾、なぜなら、\(f_2\)はフリークエント（頻繁）に\(\emptyset\)内になかった。
したがって、\(f_2 \circ f_1\)はフリークエント（頻繁）に\(T \setminus S\)内にはない。
それが意味するのは、ある\(d_1 \in D_1\)に対して、以下を満たす\({d_1}' \in D_1\)、つまり、\(d_1 \le {d_1}'\)および\(f_2 \circ f_1 ({d_1}') \in T \setminus S\)、は無い、それが含意するのは、\(d_1 \le {d_1}'\)を満たす各\({d_1}' \in D_1\)に対して、\(f_2 \circ f_1 ({d_1}') \notin T \setminus S\)、それが意味するのは、\(f_2 \circ f_1 ({d_1}') \in S\)。
それが意味するのは、\(f_2 \circ f_1\)はイベンチュアル（最終的）に\(S\)内にあること。
したがって、各\(S\)に対して、\(f_2 \circ f_1\)はイベンチュアル（最終的）に\(T \setminus S\)内にあるかイベンチュアル（最終的）に\(S\)内にあるかである。
したがって、\(f_2 \circ f_1\)はユニバーサルである。
