同一ドメイン（定義域）からのマップ（写像）たちおよび同一ドメイン（定義域）からのプロダクトセット（集合）の中へのマップ（写像）でイメージ（像）がイメージ（像）たちのプロダクトであるものに対して、サブセット（部分集合）たちのプロダクトのプリイメージ（前像）はサブセット（部分集合）たちのプリイメージ（前像）たちのインターセクション（共通集合）であることの記述/証明
話題
About: セット（集合）
この記事の目次
開始コンテキスト
- 読者は、マップ（写像）の定義を知っている。
- 読者は、プロダクトセット（集合）の定義を知っている。
ターゲットコンテキスト
- 読者は、任意の同一ドメイン（定義域）からのアンカウンタブル（不可算）かもしれない数の任意のマップ（写像）たちおよび同一ドメイン（定義域）からの当該コドメイン（余域）たちのプロダクトセット（集合）の中へのマップ（写像）でイメージ（像）がイメージ（像）たちのプロダクトであるものに対して、当該コドメイン（余域）たちの任意のサブセット（部分集合）たちのプロダクトのプリイメージ（前像）は当該サブセット（部分集合）たちのプリイメージ（前像）たちのインターセクション（共通集合）であるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述1
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(S\): \(\in \{\text{ 全てのセット（集合）たち }\}\)
\(J\): \(\in \{\text{ 全てのアンカウンタブル（不可算）かもしれないインデックスセット（集合）たち }\}\)
\(\{S'_j \in \{\text{ 全てのセット（集合）たち }\} \vert j \in J\}\):
\(\{f_j: S \to S'_j \vert j \in J\}\):
\(S'\): \(= \times_{j \in J} S'_j\)
\(f\): \(: S \to S', s \mapsto (: J \to \cup_{j \in J} S_j, j \mapsto f_j (s))\)
\(\{S_j \subseteq S'_j\} \vert j \in J\}\):
//
ステートメント（言明）たち:
\(f^{-1} (\times_{j \in J} S_j) = \cap_{j \in J} {f_j}^{-1} (S_j)\)
//
2: 証明1
全体戦略: ステップ1: \(f^{-1} (\times_{j \in J} S_j) \subseteq \cap_{j \in J} {f_j}^{-1} (S_j)\)であることを見る; ステップ2: \(\cap_{j \in J} {f_j}^{-1} (S_j) \subseteq f^{-1} (\times_{j \in J} S_j)\)であることを見る。
ステップ1:
\(p \in f^{-1} (\times_{j \in J} S_j)\)を任意のものとしよう。
\(f (p) = (:J \to \cup_{j \in J} S_j, j \mapsto f_j (p)) \in \times_{j \in J} S_j\)。
\(f_j (p) \in S_j\)、各\(j\)に対して、したがって、\(p \in {f_j}^{-1} (S_j)\)、各\(j\)に対して、したがって、\(p \in \cap_{j \in J} {f_j}^{-1} (S_j)\)。
ステップ2:
\(p \in \cap_{j \in J} {f_j}^{-1} (S_j)\)を任意のものとしよう。
\(p \in {f_j}^{-1} (S_j)\)、各\(j\)に対して。
\(f_j (p) \in S_j\)、各\(j\)に対して、\(f (p) = (: J \to \cup_{j \in J} S_j, j \mapsto f_j (p)) \in \times_{j \in J} S_j\)、したがって、\(p \in f^{-1} (\times_{j \in J} S_j)\)。
3: 構造化された記述2
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(S\): \(\in \{\text{ 全てのセット（集合）たち }\}\)
\(\{S'_1, ..., S'_n\}\): \(S'_j \in \{\text{ 全てのセット（集合）たち }\}\)
\(\{f_1, ..., f_n\}\): \(f_j: S \to S'_j\)
\(S'\): \(= S'_1 \times ... \times S'_n\)
\(f\): \(: S \to S', s \mapsto (f_1 (s), ..., f_n (s))\)
\(\{S_1, ..., S_n\}\): \(S_j \subseteq S'_j\)
//
ステートメント（言明）たち:
\(f^{-1} (S_1 \times ... \times S_n) = {f_1}^{-1} (S_1) \cap ... \cap {f_n}^{-1} (S_n)\)
//
4: 証明2
全体戦略: ステップ1: \(f^{-1} (S_1 \times ... \times S_n) \subseteq {f_1}^{-1} (S_1) \cap ... \cap {f_n}^{-1} (S_n)\)であることを見る; ステップ2: \({f_1}^{-1} (S_1) \cap ... \cap {f_n}^{-1} (S_n) \subseteq f^{-1} (S_1 \times ... \times S_n)\)であることを見る。
ステップ1:
\(p \in f^{-1} (S_1 \times ... \times S_n)\)を任意のものとしよう。
\(f (p) = (f_1 (p), ..., f_n (p)) \in S_1 \times ... \times S_n\)。
\(f_j (p) \in S_j\)、各\(j\)に対して、したがって、\(p \in {f_j}^{-1} (S_j)\)、各\(j\)に対して、したがって、\(p \in {f_1}^{-1} (S_1) \cap ... \cap {f_n}^{-1} (S_n)\)。
ステップ2:
\(p \in {f_1}^{-1} (S_1) \cap ... \cap {f_n}^{-1} (S_n)\)を任意のものとしよう。
\(p \in {f_j}^{-1} (S_j)\)、各\(j\)に対して。\(f_j (p) \in S_j\)、各\(j\)に対して。\(f (p) = (f_1 (p), f_2 (p), ..., f_n (p)) \in S_1 \times ... \times S_n\)、したがって、\(p \in f^{-1} (S_1 \times ... \times S_n)\)。
