プロダクトセット（集合）に対して、構成要素セット（集合）たちのサブセット（部分集合）たちのプロジェクション（射影）プリイメージ（前像）たちのインターセクション（共通集合）はサブセット（部分集合）たちのインターセクション（共通集合）たちのプロダクトであることの記述/証明
話題
About: セット（集合）
この記事の目次
開始コンテキスト
ターゲットコンテキスト
- 読者は、任意のアンカウンタブル（不可算）かもしれない数の構成要素セット（集合）たちの任意のプロダクトセット（集合）および構成要素セット（集合）たちの任意のサブセット（部分集合）たちに対して、当該サブセット（部分集合）たちのプロジェクション（射影）プリイメージ（前像）たちのインターセクション（共通集合）は当該サブセット（部分集合）たちのインターセクション（共通集合）たちのプロダクトであるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(J_1\): \(\in \{\text{ 全てのアンカウンタブル（不可算）かもしれないインデックスセット（集合）たち }\}\)
\(J_2\): \(\in \{\text{ 全てのアンカウンタブル（不可算）かもしれないインデックスセット（集合）たち }\}\)
\(\{S'_j \in \{\text{ 全てのセット（集合）たち }\}\vert j \in J_1\}\):
\(S'\): \(= \times_{j \in J_1} S'_j\)
\(\{S_l \in \{\text{ 全てのセット（集合）たち }\} \vert l \in J_2 \land \exists j \in J_1 (S_l \subseteq S'_j)\}\)
//
ステートメント（言明）たち:
\(\cap_{l \in J_2} {\pi_{j (l)}}^{-1} (S_l) = \times_{j \in J_1} \cap_{\{l \in J_2 \vert S_l \subseteq S'_j\}} S_l\)、ここで、"\(j (l)\)"が意味するのは、\(j\)はユニークに\(l\)によって決定される、\(S_l \subseteq S'_j\)によって、そして、\(\cap_{\emptyset} S_l = S'_j\)
//
2: 証明
全体戦略: ステップ1: \(\cap_{l \in J_2} {\pi_{j (l)}}^{-1} (S_l) \subseteq \times_{j \in J_1} \cap_{\{l \in J_2 \vert S_l \subseteq S'_j\}} S_l\)であることを見る; ステップ2: \(\times_{j \in J_1} \cap_{\{l \in J_2 \vert S_l \subseteq S'_j\}} S_l \subseteq \cap_{l \in J_2} {\pi_{j (l)}}^{-1} (S_l)\)であることを見る。
ステップ1:
\(p \in \cap_{l \in J_2} {\pi_{j (l)}}^{-1} (S_l)\)を任意のものとしよう。
\(p \in {\pi_{j (l)}}^{-1} (S_l)\)、各\(l \in J_2\)に対して、したがって、\(p_{j (l)} := \pi_{j (l)} (p) \in S_l\)、各\(l \in J_2\)に対して。
\(j \in J_1\)を、\(\{l \in J_2 \vert S_l \subseteq S'_j\} \neq \emptyset\)を満たす任意のものとしよう。
\(p_j \in \cap_{\{l \in J_2 \vert S_l \subseteq S'_j\}} S_l\)。
\(j \in J_1\)を、\(\{l \in J_2 \vert S_l \subseteq S'_j\} = \emptyset\)を満たす任意のものとしよう。
\(p_j \in S'_j = \cap_{\emptyset} S_l = \cap_{\{l \in J_2 \vert S_l \subseteq S'_j\}} S_l\)。
したがって、\(p \in \times_{j \in J_1} \cap_{\{l \in J_2 \vert S_l \subseteq S'_j\}} S_l\)。
ステップ2:
\(p \in \times_{j \in J_1} \cap_{\{l \in J_2 \vert S_l \subseteq S'_j\}} S_l\)を任意のものとしよう。
\(p_j \in \cap_{\{l \in J_2 \vert S_l \subseteq S'_j\}} S_l\)。
\(p_{j'} \in \pi_{j'} ({\pi_{j (l)}}^{-1} (S_l))\)、各\(l\)に対して？
\(j' = j (l)\)である時、\(\pi_{j'} ({\pi_{j (l)}}^{-1} (S_l)) = S_l\)、任意のセット（集合）たち間の任意のマップ（写像）に対して、コドメイン（余域）の任意のサブセット（部分集合）のプリイメージ（前像）の後のマップ（写像）コンポジション（合成）はアイデンティカル（恒等）である、もしも、当該マップ（写像）が引数サブセット（部分集合）に関してサージェクティブ（全射）である場合、という命題によって、しかし、\(p_{j'} \in \cap_{\{l' \in J_2 \vert S_{l'} \subseteq S'_{j'}\}} S_{l'}\)で\(l\)はそうしたある\(l'\)であるから、\(p_{j'} \in S_l\)、したがって、\(p_{j'} \in \pi_{j'} ({\pi_{j (l)}}^{-1} (S_l))\)。
\(j' \neq j (l)\)である時、\(\pi_{j'} ({\pi_{j (l)}}^{-1} (S_l)) = S'_l\)、しかし、\(p_{j'} \in S'_l\)であるから、\(p_{j'} \in \pi_{j'} ({\pi_{j (l)}}^{-1} (S_l))\)。
したがって、イエス、そして、\(p \in {\pi_{j (l)}}^{-1} (S_l)\)、各\(l\)に対して、したがって、\(p \in \cap_{l \in J_2} {\pi_{j (l)}}^{-1} (S_l)\)。
