プロダクトトポロジカルスペース（空間）に対して、プロジェクション（射影）はコンティニュアス（連続）であることの記述/証明
話題
About: トポロジカルスペース（空間）
この記事の目次
開始コンテキスト
- 読者は、プロダクトトポロジカルスペース（空間）の定義を知っている。
- 読者は、コンティヌアス（連続）マップ（写像）の定義を知っている。
ターゲットコンテキスト
- 読者は、任意のプロダクトトポロジカルスペース（空間）に対して、任意のプロジェクション（射影）はコンティニュアス（連続）であるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述1
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(J'\): \(\in \{\text{ アンカウンタブル（不可算）かもしれない全てのインデックスセット（集合）たち }\}\)
\(\{T_j \vert j \in J'\}\): \(T_j \in \{\text{ 全てのトポロジカルスペース（空間）たち }\}\)
\(T'\): \(= \times_{j \in J'} T_j\)で、プロダクトトポロジーを持つもの
\(J\): \(\subseteq J'\)
\(T\): \(= \times_{j \in J} T_j\)で、プロダクトトポロジーを持つもの
\(f\): \(: T' \to T, t' \mapsto (j \mapsto t' (j))\), \(= \text{ 当該プロジェクション（射影） }\)
//
ステートメント（言明）たち:
\(f \in \{\text{ 全てのコンティニュアス（連続）マップ（写像）たち }\}\)
//
2: 証明1
全体戦略: ステップ1: \(t' \in T'\)を任意のものとし、\(f (t')\)の任意のネイバーフッド（近傍）\(N_{f (t')}\)を取る; ステップ2: \(f (t')\)の以下を満たす任意のベーシック（基本）オープンネイバーフッド（開近傍）\(\times_{j \in J} U_j\)、つまり、\(f (t') \in \times_{j \in J} U_j \subseteq N_{f (t')}\)、を取る; ステップ3: 各\(j' \in J' \setminus J\)に対して、\(U_{j'} = T_{j'}\)を取り、\(U_{t'} := \times_{j' \in J'} U_{j'}\)を取り、\(U_{t'}\)は\(t'\)の\(T'\)上におけるオープンネイバーフッド（開近傍）であり\(f (U_{t'}) \subseteq N_{f (t')}\)であることを見る。
ステップ1:
\(t' \in T'\)を任意のものとしよう。
\(f (t')\)の\(T\)上における任意のネイバーフッド（近傍）を\(N_{f (t')} \subseteq T\)としよう。
ステップ2:
\(f (t')\)の以下を満たすあるベーシック（基本）オープンネイバーフッド（開近傍）\(\times_{j \in J} U_j\)、つまり、\(f (t') \in \times_{j \in J} U_j \subseteq N_{f (t')}\)、ここで、\(U_j\)は\(f (t') (j)\)の\(T_j\)上におけるオープンネイバーフッド（開近傍）、ここで、\(U_j\)たちの内のなんらかファイナイト（有限）個のものたちのみが\(T_j\)でない、がある、プロダクトトポロジーの定義によって。
ステップ3:
各\(j' \in J' \setminus J\)に対して、\(U_{j'} = T_{j'}\)を取ろう。
\(U_{t'} := \times_{j' \in J'} U_{j'} \subseteq T'\)を取ろう。
\(t' \in U_{t'}\)、なぜなら、各\(j \in J\)に対して、\(t' (j) = f (t') (j) \in U_j\)、そして、各\(j' \in J' \setminus J\)に対して、\(t' (j') \in T_{j'} = U_{j'}\)。
\(U_{t'}\)は\(T'\)上でオープン（開）である、プロダクトトポロジーの定義によって: \(U_{j'}\)たちの内のなんらかファイナイト（有限）個のものたちだけが\(T_{j'}\)たちでない。
したがって、\(U_{t'}\)は\(t'\)の\(T'\)上におけるオープンネイバーフッド（開近傍）である。
\(f (U_{t'}) \subseteq \times_{j \in J} U_j\)（実のところ、\(=\)が成立する、しかし、\(\subseteq\)で十分である、私たちの目的のためには）、なぜなら、各\(t'' \in U_{t'}\)に対して、各\(j \in J\)に対して、\(f (t'') (j) = t'' (j) \subseteq U_j\)。
したがって、\(f (U_{t'}) \subseteq \times_{j \in J} U_j \subseteq N_{f (t')}\)。
1: 構造化された記述2
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(J'\): \(= \{1, ..., n\}\)
\(\{T_1, ..., T_n\}\): \(T_j \in \{\text{ 全てのトポロジカルスペース（空間）たち }\}\)
\(T'\): \(= T_1 \times ... \times T_n\)でプロダクトトポロジーを持つもの
\(J\): \(\subseteq J'\), \(= \{j_1, ..., j_m\}\)
\(T\): \(= T_{j_1} \times ... \times T_{j_m}\)でプロダクトトポロジーを持つもの
\(f\): \(: T' \to T, (t'^1, ..., t'^n) \mapsto (t'^{j_1}, ..., t'^{j_m})\), \(= \text{ 当該プロジェクション（射影） }\)
//
ステートメント（言明）たち:
\(f \in \{\text{ 全てのコンティニュアス（連続）マップ（写像）たち }\}\)
//
4: 証明2
全体戦略: ステップ1: \(t' \in T'\)を任意のものとし、\(f (t')\)の任意のネイバーフッド（近傍）\(N_{f (t')}\)を取る; ステップ2: \(f (t')\)の以下を満たす任意のベーシック（基本）オープンネイバーフッド（開近傍）\(U_{j_1} \times ... \times U_{j_m}\)、つまり、\(f (t') \in U_{j_1} \times ... \times U_{j_m} \subseteq N_{f (t')}\)、を取る; ステップ3: 各\(j' \in J' \setminus J\)に対して、\(U_{j'} = T_{j'}\)を取り、\(U_{t'} := U_1 \times ... \times U_n\)を取り、\(U_{t'}\)は\(t'\)の\(T'\)上におけるオープンネイバーフッド（開近傍）であり\(f (U_{t'}) \subseteq N_{f (t')}\)であることを見る。
ステップ1:
\(t' \in T'\)を任意のものとしよう。
\(f (t')\)の\(T\)上における任意のネイバーフッド（近傍）を\(N_{f (t')} \subseteq T\)としよう。
ステップ2:
\(f (t')\)の以下を満たすあるベーシック（基本）オープンネイバーフッド（開近傍）\(U_{j_1} \times ... \times U_{j_m}\)、つまり、\(f (t') \in U_{j_1} \times ... \times U_{j_m} \subseteq N_{f (t')}\)、ここで、\(U_{j_l}\)は\((f (t'))^{j_l}\)の\(T_{j_l}\)上におけるオープンネイバーフッド（開近傍）、がある、プロダクトトポロジーの定義によって。
ステップ3:
各\(j' \in J' \setminus J\)に対して、\(U_{j'} = T_{j'}\)を取ろう。
\(U_{t'} := U_1 \times ... \times U_n \subseteq T'\)を取ろう。
\(t' \in U_{t'}\)、なぜなら、各\(j \in J\)に対して、\(t'^j = (f (t'))^j \in U_j\)、そして、各\(j' \in J' \setminus J\)に対して、\(t'^{j'} \in T_{j'} = U_{j'}\)。
\(U_{t'}\)は\(T'\)上でオープン（開）である、プロダクトトポロジーの定義によって。
したがって、\(U_{t'}\)は\(t'\)の\(T'\)上におけるオープンネイバーフッド（開近傍）である。
\(f (U_{t'}) \subseteq U_{j_1} \times ... \times U_{j_m}\)（実のところ、\(=\)が成立する、しかし、\(\subseteq\)で十分である、私たちの目的のためには）、なぜなら、各\(t'' \in U_{t'}\)に対して、各\(j \in J\)に対して、\((f (t''))^j = t''^j \subseteq U_j\)。
したがって、\(f (U_{t'}) \subseteq U_{j_1} \times ... \times U_{j_m} \subseteq N_{f (t')}\)。
