マップ（写像）、ドメイン（定義域）のサブセット（部分集合）、コドメイン（余域）のサブセット（部分集合）に対して、サブセット（部分集合）のイメージ（像）はサブセット（部分集合）内に包含されサブセット（部分集合）のコンプリメント（補集合）のイメージ（像）はサブセット（部分集合）のコンプリメント（補集合）内に包含される、もしも、サブセット（部分集合）のプリイメージ（前像）がサブセット（部分集合）でありサブセット（部分集合）のコンプリメント（補集合）のプリイメージ（前像）がサブセット（部分集合）のコンプリメント（補集合）である場合、そしてその場合に限って、ことの記述/証明
話題
About: セット（集合）
この記事の目次
開始コンテキスト
- 読者は、マップ（写像）の定義を知っている。
ターゲットコンテキスト
- 読者は、任意のマップ（写像）、ドメイン（定義域）の任意のサブセット（部分集合）、コドメイン（余域）の任意のサブセット（部分集合）に対して、当該サブセット（部分集合）のイメージ（像）は当該サブセット（部分集合）内に包含され当該サブセット（部分集合）のコンプリメント（補集合）のイメージ（像）は当該サブセット（部分集合）のコンプリメント（補集合）内に包含される、もしも、当該サブセット（部分集合）のプリイメージ（前像）が当該サブセット（部分集合）であり当該サブセット（部分集合）のコンプリメント（補集合）のプリイメージ（前像）が当該サブセット（部分集合）のコンプリメント（補集合）である場合、そしてその場合に限って、という命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(S'_1\): \(\in \{\text{ 全てのセット（集合）たち }\}\)
\(S'_2\): \(\in \{\text{ 全てのセット（集合）たち }\}\)
\(f\): \(S'_1 \to S'_2\)
\(S_1\): \(\subseteq S'_1\)
\(S_2\): \(\subseteq S'_2\)
//
ステートメント（言明）たち:
(
\(f (S_1) \subseteq S_2\)
\(\land\)
\(f (S'_1 \setminus S_1) \subseteq S'_2 \setminus S_2\)
)
\(\iff\)
(
\(S_1 = f^{-1} (S_2)\)
\(\land\)
\(S'_1 \setminus S_1 = f^{-1} (S'_2 \setminus S_2)\)
).
//
2: 自然言語記述
任意のセット（集合）たち\(S'_1, S'_2\)、任意のマップ（写像）\(f: S'_1 \to S'_2\)、任意のサブセット（部分集合）たち\(S_1 \subseteq S'_1, S_2 \subseteq S'_2\)に対して、\(f (S_1) \subseteq S_2\)および\(f (S'_1 \setminus S_1) \subseteq S'_2 \setminus S_2\)、もしも、\(S_1 = f^{-1} (S_2)\)および\(S'_1 \setminus S_1 = f^{-1} (S'_2 \setminus S_2)\)である場合、そしてその場合に限って。
3: 証明
全体戦略: ステップ1: \(f (S_1) \subseteq S_2\)および\(f (S'_1 \setminus S_1) \subseteq S'_2 \setminus S_2\)と仮定し、\(S_1 = f^{-1} (S_2)\)および\(S'_1 \setminus S_1 = f^{-1} (S'_2 \setminus S_2)\)であることを見る; ステップ2: \(S_1 = f^{-1} (S_2)\)および\(S'_1 \setminus S_1 = f^{-1} (S'_2 \setminus S_2)\)と仮定し、\(f (S_1) \subseteq S_2\)および\(f (S'_1 \setminus S_1) \subseteq S'_2 \setminus S_2\)であることを見る。
ステップ1:
\(f (S_1) \subseteq S_2\)および\(f (S'_1 \setminus S_1) \subseteq S'_2 \setminus S_2\)であると仮定する。
\(S_1 \subseteq f^{-1} (S_2)\)は即座である。
\(f^{-1} (S_2) \subseteq S_1\)であることを証明しよう。任意の\(p \in f^{-1} (S_2)\)に対して、\(f (p) \in S_2\)、\(f (p) \notin S'_2 \setminus S_2\)、\(f (p) \notin f (S'_1 \setminus S_1)\)、\(p \notin S'_1 \setminus S_1\)、したがって、\(p \in S_1\) as \(p \in S'_1\)。
\(S'_1 \setminus S_1 \subseteq f^{-1} (S'_2 \setminus S_2)\)は即座である。
\(f^{-1} (S'_2 \setminus S_2) \subseteq S'_1 \setminus S_1\)であることを証明しよう。任意の\(p \in f^{-1} (S'_2 \setminus S_2)\)に対して、\(f (p) \in S'_2 \setminus S_2\)、\(f (p) \notin S_2\)、\(f (p) \in S'_2\)であるから、\(p \notin S_1\)、したがって、\(p \in S'_1 \setminus S_1\)、\(p \in S'_1\)であるから。
ステップ2:
\(S_1 = f^{-1} (S_2)\)および\(S'_1 \setminus S_1 = f^{-1} (S'_2 \setminus S_2)\)であると仮定しよう。
\(f (S_1) \subseteq S_2\)および\(f (S'_1 \setminus S_1) \subseteq S'_2 \setminus S_2\)は即座である。
