マップ（写像）、ドメイン（定義域）のサブセット（部分集合）、コドメイン（余域）のポイントに対して、もしも、ポイントのプリイメージ（前像）とサブセット（部分集合）のインターセクション（共通集合）がプリイメージ（前像）である場合、ポイントのプリイメージ（前像）は、サブセット（部分集合）内に包含されているまたはサブセット（部分集合）からディスジョイント（互いに素）であることの記述/証明
話題
About: セット（集合）
この記事の目次
開始コンテキスト
ターゲットコンテキスト
- 読者は、任意のマップ（写像）、当該ドメイン（定義域）の任意のサブセット（部分集合）、当該コドメイン（余域）の任意のポイントに対して、もしも、当該ポイントのプリイメージ（前像）と当該サブセット（部分集合）のインターセクション（共通集合）があるプリイメージ（前像）である場合、当該ポイントのプリイメージ（前像）は、当該サブセット（部分集合）内に包含されているまたは当該サブセット（部分集合）からディスジョイント（互いに素）であるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(S'_1\): \(\in \{\text{ 全てのセット（集合）たち }\}\)
\(S'_2\): \(\in \{\text{ 全てのセット（集合）たち }\}\)
\(f\): \(: S'_1 \to S'_2\)
\(S_1\): \(\subseteq S'_1\)
\(s'_2\): \(\in S'_2\)
//
ステートメント（言明）たち:
\(\exists S_2 \subseteq S'_2 (f^{-1} (s'_2) \cap S_1 = f^{-1} (S_2))\)
\(\implies\)
\(f^{-1} (s'_2) \subseteq S_1 \lor f^{-1} (s'_2) \cap S_1 = \emptyset\)
//
2: 注
\(s'_2\)は、あるサブセット（部分集合）\({S'_2}^` \subseteq S'_2\)で置き換えることはできない、本命題にとって: 各\(s'_2 \in {S'_2}^`\)に対して、本命題は成立する、しかし、何らかの、\(s'_2 \neq \widetilde{s'_2}\)を満たす\(s'_2, \widetilde{s'_2} \in {S'_2}^`\)に対して、\(f^{-1} (s'_2) \subseteq S_1\)かつ\(f^{-1} (\widetilde{s'_2}) \cap S_1 = \emptyset\)であるかもしれない、例えば、すると、\(f^{-1} ({S'_2}^`) \subseteq S_1 \lor f^{-1} ({S'_2}^`) \cap S_1 = \emptyset\)は成立しない。
例えば、\(f: \{0, 1\} \to \{0, 1\} = id\)、\(S_1 = \{1\}\)、\(S_2 = \{0, 1\}\)としよう、すると、\(f^{-1} (\{0, 1\}) = \{0, 1\}\)および\(f^{-1} (\{0, 1\}) \cap \{1\} = \{1\} = f^{-1} (\{1\})\)、しかし、\(\{0, 1\} \subseteq \{1\}\)でも\(\{0, 1\} \cap \{1\} = \emptyset\)も成立しない: \(s'_2 = 0\)に対して、\(f^{-1} (0) = \{0\}\)および\(f^{-1} (0) \cap \{1\} = \emptyset = f^{-1} (\emptyset)\)、そして、\(f^{-1} (0) \cap \{1\} = \emptyset\)が成立する; \(s'_2 = 1\)に対して、\(f^{-1} (1) = \{1\}\)および\(f^{-1} (1) \cap \{1\} = \{1\} = f^{-1} (\{1\})\)、そして、\(f^{-1} (1) \subseteq \{1\}\)が成立する。
3: 証明
全体戦略: ステップ1: \(f^{-1} (s'_2) \cap S_1 \neq \emptyset\)であると仮定し、\(f^{-1} (s'_2) \subseteq S_1\)であることを見る。
ステップ1:
\(f^{-1} (s'_2) \cap S_1 \neq \emptyset\)であると仮定しよう。
\(s'_2 \notin S_2\)であると仮定しよう。
\(f^{-1} (s'_2) \cap f^{-1} (S_2) = \emptyset\)、任意のディスジョイント（互いに素な）サブセット（部分集合）たちの任意のマップ（写像）下のプリイメージ（前像）たちはディスジョイント（互いに素）であるという命題によって。
\(s_1 \in f^{-1} (s'_2) \cap S_1\)を任意のものとしよう。
\(s_1 \in f^{-1} (s'_2) \cap S_1 = f^{-1} (S_2)\)、\(f^{-1} (s'_2) \cap f^{-1} (S_2) = \emptyset\)に反する矛盾。
したがって、\(s'_2 \in S_2\)。
したがって、\(f^{-1} (s'_2) \subseteq f^{-1} (S_2) = f^{-1} (s'_2) \cap S_1 \subseteq S_1\)。
したがって、\(f^{-1} (s'_2) \cap S_1 = \emptyset\)または\(f^{-1} (s'_2) \subseteq S_1\)。
