\(2\)個のセット（集合）たちのプロダクトからセット（集合）の中へのマップ（写像）、第2セット（集合）のサブセット（部分集合）、第3セット（集合）のサブセット（部分集合）に対して、第1セット（集合）のサブセット（部分集合）でポイントと第2セット（集合）のサブセット（部分集合）のプロダクトのイメージ（像）が第3セット（集合）のサブセット（部分集合）内に包含されているもののコンプリメント（補集合）は、第3セット（集合）のサブセット（部分集合）のコンプリメント（補集合）のプリイメージ（前像）と第1セット（集合）と第2セット（集合）のサブセット（部分集合）のプロダクトのインターセクション（共通集合）のプロジェクション（射影）であることの記述/証明
話題
About: セット（集合）
この記事の目次
開始コンテキスト
- 読者は、プロダクトセット（集合）の定義を知っている。
- 読者は、プロダクトセット（集合）からサブプロダクトセット（集合）の上へのプロジェクション（射影）の定義を知っている。
- 読者は、コドメイン（余域）のサブセット（部分集合）のマップ（写像）プリイメージ（前像）の定義を知っている。
ターゲットコンテキスト
- 読者は、任意の\(2\)個のセット（集合）たちのプロダクトから任意のセット（集合）の中への任意のマップ（写像）、第2セット（集合）の任意のサブセット（部分集合）、第3セット（集合）の任意のサブセット（部分集合）に対して、第1セット（集合）のサブセット（部分集合）で各ポイントと第2セット（集合）の当該サブセット（部分集合）のプロダクトのイメージ（像）が第3セット（集合）の当該サブセット（部分集合）内に包含されているもののコンプリメント（補集合）は、第3セット（集合）の当該サブセット（部分集合）のコンプリメント（補集合）のプリイメージ（前像）と第1セット（集合）と第2セット（集合）の当該サブセット（部分集合）のプロダクトのインターセクション（共通集合）のプロジェクション（射影）であるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(S_1\): \(\in \{\text{ 全てのセット（集合）たち }\}\)
\(S_2\): \(\in \{\text{ 全てのセット（集合）たち }\}\)
\(S_3\): \(\in \{\text{ 全てのセット（集合）たち }\}\)
\(f\): \(: S_1 \times S_2 \to S_3\)
\({S_2}^`\): \(\subseteq S_2\)
\({S_3}^`\): \(\subseteq S_3\)
\(\pi_1\): \(: S_1 \times S_2 \to S_1, (s_1, s_2) \mapsto s_1\)
//
ステートメント（言明）たち:
\(S_1 \setminus \{s_1 \in S_1 \vert f (\{s_1\} \times {S_2}^`) \subseteq {S_3}^`\} = \pi_1 (f^{-1} (S_3 \setminus {S_3}^`) \cap (S_1 \times {S_2}^`))\)
//
2: 証明
全体戦略: ステップ1: 各\(s_1 \in S_1 \setminus \{s_1 \in S_1 \vert f (\{s_1\} \times {S_2}^`) \subseteq {S_3}^`\}\)に対して、\(s_1 \in \pi_1 (f^{-1} (S_3 \setminus {S_3}^`) \cap (S_1 \times {S_2}^`))\)であることを見る; ステップ2: 各\(s_1 \in \pi_1 (f^{-1} (S_3 \setminus {S_3}^`) \cap (S_1 \times {S_2}^`))\)に対して、\(s_1 \in S_1 \setminus \{s_1 \in S_1 \vert f (\{s_1\} \times {S_2}^`) \subseteq {S_3}^`\}\)であることを見る; ステップ3: 本命題を結論する。
ステップ1:
\(s_1 \in S_1 \setminus \{s_1 \in S_1 \vert f (\{s_1\} \times {S_2}^`) \subseteq {S_3}^`\}\)を任意のものとしよう。
\(s_1 \notin \{s_1 \in S_1 \vert f (\{s_1\} \times {S_2}^`) \subseteq {S_3}^`\}\)、それが意味するのは、\(f (\{s_1\} \times {S_2}^`) \subseteq {S_3}^`\)は成立しないということ。
それが意味するのは、以下を満たすある\({s_2}^` \in {S_2}^`\)、つまり、\(f ((s_1, {s_2}^`)) \notin {S_3}^`\)、があるということ。
\(f ((s_1, {s_2}^`)) \in S_3 \setminus {S_3}^`\)、したがって、\((s_1, {s_2}^`) \in f^{-1} (S_3 \setminus {S_3}^`)\)。
\((s_1, {s_2}^`) \in S_1 \times {S_2}^`\)でもある、したがって、\((s_1, {s_2}^`) \in f^{-1} (S_3 \setminus {S_3}^`) \cap (S_1 \times {S_2}^`)\)。
したがって、\(s_1 = \pi_1 ((s_1, {s_2}^`)) \in \pi_1 (f^{-1} (S_3 \setminus {S_3}^`) \cap (S_1 \times {S_2}^`))\)。
したがって、\(S_1 \setminus \{s_1 \in S_1 \vert f (\{s_1\} \times {S_2}^`) \subseteq {S_3}^`\} \subseteq \pi_1 (f^{-1} (S_3 \setminus {S_3}^`) \cap (S_1 \times {S_2}^`))\)。
ステップ2:
\(s_1 \in \pi_1 (f^{-1} (S_3 \setminus {S_3}^`) \cap (S_1 \times {S_2}^`))\)を任意のものとしよう。
以下を満たすある\(s_2 \in S_2\)、つまり、\((s_1, s_2) \in f^{-1} (S_3 \setminus {S_3}^`) \cap (S_1 \times {S_2}^`)\)、がある。
\(f ((s_1, s_2)) \in S_3 \setminus {S_3}^`\)および\(s_2 \in {S_2}^`\)。
\(f ((s_1, s_2)) \notin {S_3}^`\)。
したがって、\(f (\{s_1\} \times {S_2}^`) \subseteq {S_3}^`\)は成立しない。
したがって、\(s_1 \notin \{s_1 \in S_1 \vert f (\{s_1\} \times {S_2}^`) \subseteq {S_3}^`\}\)。
したがって、\(s_1 \in S_1 \setminus \{s_1 \in S_1 \vert f (\{s_1\} \times {S_2}^`) \subseteq {S_3}^`\}\)。
したがって、\(\pi_1 (f^{-1} (S_3 \setminus {S_3}^`) \cap (S_1 \times {S_2}^`)) \subseteq S_1 \setminus \{s_1 \in S_1 \vert f (\{s_1\} \times {S_2}^`) \subseteq {S_3}^`\}\)。
ステップ3:
したがって、\(S_1 \setminus \{s_1 \in S_1 \vert f (\{s_1\} \times {S_2}^`) \subseteq {S_3}^`\} = \pi_1 (f^{-1} (S_3 \setminus {S_3}^`) \cap (S_1 \times {S_2}^`))\)。
