プリイメージ（前像）の後のマップ（写像）コンポジション（合成）はアイデンティカル（恒等）である、もしも、マップ（写像）が引数サブセット（部分集合）に関してサージェクティブ（全射）である場合、ことの記述/証明
話題
About: セット（集合）
この記事の目次
開始コンテキスト
ターゲットコンテキスト
- 読者は、任意のセット（集合）たち間の任意のマップ（写像）に対して、コドメイン（余域）の任意のサブセット（部分集合）のプリイメージ（前像）の後のマップ（写像）コンポジション（合成）はアイデンティカル（恒等）である、もしも、当該マップ（写像）が引数サブセット（部分集合）に関してサージェクティブ（全射）である場合、という命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(S'_1\): \(\in \{\text{ 全てのセット（集合）たち }\}\)
\(S'_2\): \(\in \{\text{ 全てのセット（集合）たち }\}\)
\(f\): \(: S'_1 \to S'_2\)
\(S_2\): \(\subseteq S'_2\)
//
ステートメント（言明）たち:
\(\forall p \in S_2 (p \in f (S'_1))\)
\(\implies\)
\(f \circ f^{-1} (S_2) = S_2\)
//
\(f\)がサージェクティブ（全射）である時は、当該条件は、\(S'_2\)の任意のサブセット（部分集合）に対して満たされる。
2: 自然言語記述
任意のセット（集合）たち\(S'_1, S'_2\)、任意のマップ（写像）\(f: S'_1 \to S'_2\)、任意のサブセット（部分集合）\(S_2 \subseteq S'_2\)に対して、もしも、\(f\)が\(S_2\)に関してサージェクティブ（全射）である（それが意味するのは、\(S_2\)上の任意のポイントは\(f\)のレンジ（値域）内にいるということ）場合、\(f \circ f^{-1} (S_2) = S_2\)。
\(f\)がサージェクション（全射）である時は、\(f\)は\(S'_2\)の任意のサブセット（部分集合）に関してサージェクティブ（全射）である。
3: 証明
全体戦略: ステップ1: 一般に\(f \circ f^{-1} (S_2) \subseteq S_2\)であることを見る; ステップ2: \(\forall p \in S_2 (p \in f (S'_1))\)であると仮定し、\(S_2 \subseteq f \circ f^{-1} (S_2)\)であることを見る。
ステップ1:
\(f \circ f^{-1} (S_2) \subseteq S_2\)、任意のセット（集合）間マップ（写像）に対して、任意のプリイメージ（前像）の後のそのマップ（写像）によるコンポジション（合成）は引数セット（集合）の中に包含されているという命題によって。
したがって、それは、\(S_2 \subseteq f \circ f^{-1} (S_2)\)という問題である。
ステップ2:
\(S_2 \subseteq f \circ f^{-1} (S_2)\)であることを見よう。
\(\forall p \in S_2 (p \in f (S'_1))\)であると仮定しよう。
任意の\(p \in S_2\)に対して、ある\(p' \in f^{-1} (p) \subseteq f^{-1} (S_2)\)がある。\(p = f (p') \in f \circ f^{-1} (p) \subseteq f \circ f^{-1} (S_2)\)。
