プロダクトマップ（写像）に対して、プロダクトサブセット（部分集合）のイメージ（像）は、コンポーネントサブセット（部分集合）たちのコンポーネントたちマップ（写像）たち下のイメージ（像）たちのプロダクトであることの記述/証明
話題
About: セット（集合）
この記事の目次
開始コンテキスト
- 読者は、プロダクトマップ（写像）の定義を知っている。
ターゲットコンテキスト
- 読者は、任意のプロダクトマップ（写像）に対して、任意のプロダクトサブセット（部分集合）のイメージ（像）は、当該コンポーネントサブセット（部分集合）たちの当該コンポーネントたちマップ（写像）たち下のイメージ（像）たちのプロダクトであるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(J\): \(\in \{\text{ 全てのアンカウンタブル（不可算）かもしれないインデックスセット（集合）たち }\}\)
\(\{S_{1, j} \vert j \in J\}\): \(S_{1, j} \in \{\text{ 全てのセット（集合）たち }\}\)
\(\{S_{2, j} \vert j \in J\}\): \(S_{2, j} \in \{\text{ 全てのセット（集合）たち }\}\)
\(\{f_j \vert j \in J\}\): \(f_j: S_{1, j} \to S_{2, j}\)
\(\{S^`_{1, j} \vert j \in J\}\): \(S^`_{1, j} \subseteq S_{1, j}\)
//
ステートメント（言明）たち:
\((\times_{j \in J} f_j) (\times_{j \in J} S^`_{1, j}) = \times_{j \in J} f_j (S^`_{1, j})\)
//
2: 注
プロダクトマップ（写像）の定義内にて、"記述1"によるプロダクトマップ（写像）と"記述2"によるプロダクトマップ（写像）は厳密には同じではないが、当該2個の定義たちに対する"証明"のロジックたちは基本的に同じなので、"証明"はそれらを区別しない。
記法として、任意の\(s \in \times_{j \in J} S_{l, j}\)に対して、\(s^m\)は\(s\)の\(m\)-コンポーネントを示す。
3: 証明
全体戦略: ステップ1: \((\times_{j \in J} f_j) (\times_{j \in J} S^`_{1, j}) \subseteq \times_{j \in J} f_j (S^`_{1, j})\)であることを見る; ステップ2: \(\times_{j \in J} f_j (S^`_{1, j}) \subseteq (\times_{j \in J} f_j) (\times_{j \in J} S^`_{1, j})\)であることを見る; ステップ3: 本命題を結論する。
ステップ1:
\(s \in (\times_{j \in J} f_j) (\times_{j \in J} S^`_{1, j})\)を任意のものとしよう。
以下を満たすある\(s' \in \times_{j \in J} S^`_{1, j}\)、つまり、\(s = (\times_{j \in J} f_j) (s')\)、がある。
\(s' \in \times_{j \in J} S^`_{1, j}\)が意味するのは、\(s'^j \in S^`_{1, j}\)、したがって、\(f_j (s'^j) \in f_j (S^`_{1, j})\)。
\(s = (\times_{j \in J} f_j) (s') = \times_{j \in J} f_j (s'^j) \subseteq \times_{j \in J} f_j (S^`_{1, j})\)。
したがって、\((\times_{j \in J} f_j) (\times_{j \in J} S^`_{1, j}) \subseteq \times_{j \in J} f_j (S^`_{1, j})\)。
ステップ2:
\(s \in \times_{j \in J} f_j (S^`_{1, j})\)を任意のものとしよう。
\(s^j \in f_j (S^`_{1, j})\)。
以下を満たすある\(s'^j \in S^`_{1, j}\)、つまり、\(s^j = f_j (s'^j)\)、がある。
\(\times_{j \in J} s'^j \in \times_{j \in J} S^`_{1, j}\)。
\(s = \times_{j \in J} s^j = (\times_{j \in J} f_j) (\times_{j \in J} s'^j) \in (\times_{j \in J} f_j) (\times_{j \in J} S^`_{1, j})\)。
したがって、\(\times_{j \in J} f_j (S^`_{1, j}) \subseteq (\times_{j \in J} f_j) (\times_{j \in J} S^`_{1, j})\)。
ステップ3:
したがって、\((\times_{j \in J} f_j) (\times_{j \in J} S^`_{1, j}) = \times_{j \in J} f_j (S^`_{1, j})\)。
