ファイナイト（有限）プロダクトセット（集合）はセット（集合）たちの逐次プロダクトたちへ'セット（集合）たち - マップ（写像）たち'アイソモーフィック（同形写像）であることの記述/証明
話題
About: セット（集合）
この記事の目次
開始コンテキスト
- 読者は、プロダクトセット（集合）の定義を知っている。
- 読者は、%カテゴリー名%アイソモーフィズム（同形写像）の定義を知っている。
ターゲットコンテキスト
- 読者は、任意のファイナイト（有限）プロダクトセット（集合）は当該セット（集合）たちの逐次プロダクトたちへ'セット（集合）たち - マップ（写像）たち'アイソモーフィック（同形写像）であるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(J\): \(\in \{\text{ 全てのファイナイト（有限）インデックスセット（集合）たち }\}\)で、\(\vert J \vert = n\)および任意のオーダリング（順序）を持つもの
\(\{S_j \in \{\text{ 全てのセット（集合）たち } \} \vert j \in J\}\):
\(\times_{j \in J} S_j\):
\(( ... ((S_{J_1} \times S_{J_2}) \times S_{J_3}) \times ... ) \times S_{J_n}\):
//
ステートメント（言明）たち:
\(\times_{j \in J} S_j \cong_{sets} ( ... ((S_{J_1} \times S_{J_2}) \times S_{J_3}) \times ... ) \times S_{J_n}\)
//
2: 証明
全体戦略: ステップ1: あるバイジェクション（全単射）\(g: \times_{j \in J} S_j \to ( ... ((S_{J_1} \times S_{J_2}) \times S_{J_3}) \times ... ) \times S_{J_n}\)を定義する。
ステップ1:
マップ（写像）\(g: \times_{j \in J} S_j \to ( ... ((S_{J_1} \times S_{J_2}) \times S_{J_3}) \times ... ) \times S_{J_n}, f \mapsto f_{n - 1}\)を定義しよう、ここで、\(f_1 \in S_{J_1} \times S_{J_2}\)（それは、\(\{1, 2\}\)から\(S_{J_1} \cup S_{J_2}\)の中へのあるマップ（写像）である）は、\(f_1 (1) = f (J_1)\)および\(f_1 (2) = f (J_2)\)として決定され、\(f_2 \in (S_{J_1} \times S_{J_2}) \times S_{J_3}\)（それは、\(\{1, 2\}\)から\((S_{J_1} \times S_{J_2}) \cup S_{J_3}\)の中へのあるマップ（写像）である）は、\(f_2 (1) = f_1\)および\(f_2 (2) = f (J_3)\)として決定され、...、そして、\(f_{n - 1} \in ( ... ((S_{J_1} \times S_{J_2}) \times S_{J_3}) \times ... ) \times S_{J_n}\)（それは、\(\{1, 2\}\)から\(( ... ((S_{J_1} \times S_{J_2}) \times S_{J_3}) \times ... ) \times S_{J_{n - 1}} \cup S_{J_n}\)の中へのあるマップ（写像）である）は、\(f_{n - 1} (1) = f_{n - 1}\)および\(f_{n - 1} (2) = f (J_n)\)として決定される。
\(g\)はあるインジェクション（単射）である、なぜなら、以下を満たす任意の\(f, f' \in \times_{j \in J} S_j\)、つまり、\(f \neq f'\)、に対して、\(f (J_{n'}) \neq f' (J_{n'})\)、ある\(n'\)に対して、そして、\(n' = 1\)である時は、\(f_1 \neq f'_1\)、なぜなら、\(f_1 (1) = f (J_1) \neq f' (J_1) = f'_1 (1)\)、そして、そうでない時は、\(f_{n' - 1} \neq f'_{n' - 1}\)、なぜなら、\(f_{n' - 1} (2) = f (J_{n'}) \neq f' (J_{n'}) = f'_{n' - 1} (2)\)、すると、\(f_{n - 1} \neq f'_{n - 1}\)。
\(g\)はあるサージェクション（全射）である、なぜなら、各\(f_{n - 1} \in ( ... ((S_{J_1} \times S_{J_2}) \times S_{J_3}) \times ... ) \times S_{J_n}\)に対して、以下を満たす\(f \in \times_{j \in J} S_j\)、つまり、\(f (J_1) = f_1 (1)\)、\(f (J_2) = f_1 (2)\), \(f (J_3) = f_2 (2)\)、...、\(f (J_n) = f_{n - 1} (2)\)、\(g (f) = f_{n - 1}\)、がある。
したがって、\(g\)はあるバイジェクション（全単射）である。
