セット（集合）でイクイバレンスリレーション（同値関係）を持つもの、サブセット（部分集合）、クオシエント（商）セット（集合）からクオシエント（商）セット（集合）の中へのカノニカル（正典）インジェクション（単射）、サブセット（部分集合）のクオシエント（商）セット（集合）のサブセット（部分集合）に対して、サブセット（部分集合）のカノニカル（正典）インジェクション（単射）下のイメージ（像）のクラシフィケーションマップ（クラス分け写像）下のプリイメージ（前像）はサブセット（部分集合）のクラシフィケーションマップ（クラス分け写像）下のプリイメージ（前像）のサチュレーション（飽和）であることの記述/証明
話題
About: セット（集合）
この記事の目次
開始コンテキスト
- 読者は、クオシエント（商）セット（集合）の定義を知っている。
- 読者は、セット（集合）でイクイバレンスリレーション（同値関係）を持つもののサブセット（部分集合）のサチュレーション（飽和）の定義を知っている。
- 読者は、コドメイン（余域）のサブセット（部分集合）のマップ（写像）プリイメージ（前像）の定義を知っている。
- 読者は、任意のセット（集合）で任意のイクイバレンスリレーション（同値関係）を持つものおよび任意のサブセット（部分集合）で当該サブセット（部分集合）イクイバレンスリレーション（同値関係）を持つものに対して、当該サブセット（部分集合）のクオシエント（商）セット（集合）から当該セット（集合）のクオシエント（商）セット（集合）の中へのカノニカル（正典）インジェクション（単射）があるという命題を認めている。
ターゲットコンテキスト
- 読者は、任意のセット（集合）で任意のイクイバレンスリレーション（同値関係）を持つもの、任意のサブセット（部分集合）、当該サブセット（部分集合）のクオシエント（商）セット（集合）から当該セット（集合）のクオシエント（商）セット（集合）の中へのカノニカル（正典）インジェクション（単射）、当該サブセット（部分集合）のクオシエント（商）セット（集合）の任意のサブセット（部分集合）に対して、当該サブセット（部分集合）のカノニカル（正典）インジェクション（単射）下のイメージ（像）の当該セット（集合）のクラシフィケーションマップ（クラス分け写像）下のプリイメージ（前像）は当該サブセット（部分集合）の当該サブセット（部分集合）のクラシフィケーションマップ（クラス分け写像）下のプリイメージ（前像）のサチュレーション（飽和）であるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(S'\): \(\in \{\text{ 全てのセット（集合）たち }\}\)で、任意のイクイバレンスリレーション（同値関係）\(\sim'\)を持つもの
\(S\): \(\subseteq S'\)で、サブセット（部分集合）イクイバレンスリレーション（同値関係）\(\sim\)を持つもの
\(f'\): \(: S' \to S' / \sim', s' \mapsto [s']'\)
\(f\): \(: S \to S / \sim, s \mapsto [s]\)
\(g\): \(: S / \sim \to S' / \sim', [s] \mapsto [s]'\)
\(\widetilde{S}\): \(\subseteq S / \sim\)
//
ステートメント（言明）たち:
\(f'^{-1} (g (\widetilde{S})) = Sat (f^{-1} (\widetilde{S}), \sim')\)
//
2: 証明
全体戦略: ステップ1: 各\(p \in f'^{-1} (g (\widetilde{S}))\)に対して、\(p \in Sat (f^{-1} (\widetilde{S}), \sim')\)であることを見る; ステップ2: 各\(p \in Sat (f^{-1} (\widetilde{S}), \sim')\)に対して、\(p \in f'^{-1} (g (\widetilde{S}))\)であることを見る。
ステップ1:
\(p \in f'^{-1} (g (\widetilde{S}))\)を任意のものとしよう。
\(f' (p) \in g (\widetilde{S})\)。
以下を満たすある\([s] \in \widetilde{S}\)、つまり、\(f' (p) = g ([s])\)、がある。
しかし、\(g ([s]) = g (f (s)) = f' \vert_{S} (s)\)、任意のセット（集合）で任意のイクイバレンスリレーション（同値関係）を持つものおよび任意のサブセット（部分集合）で当該サブセット（部分集合）イクイバレンスリレーション（同値関係）を持つものに対して、当該サブセット（部分集合）のクオシエント（商）セット（集合）から当該セット（集合）のクオシエント（商）セット（集合）の中へのカノニカル（正典）インジェクション（単射）があるという命題によって、\(= f' (s)\)。
したがって、\(f' (p) = f' (s)\)、それが意味するのは、\(p \sim' s\)。
\(g (f (s)) = g ([s]) = f' (p) \in g (\widetilde{S})\)。
\(g\)はあるインジェクション（単射）であるから、任意のセット（集合）で任意のイクイバレンスリレーション（同値関係）を持つものおよび任意のサブセット（部分集合）で当該サブセット（部分集合）イクイバレンスリレーション（同値関係）を持つものに対して、当該サブセット（部分集合）のクオシエント（商）セット（集合）から当該セット（集合）のクオシエント（商）セット（集合）の中へのカノニカル（正典）インジェクション（単射）があるという命題によって、\(f (s) \in \widetilde{S}\)、なぜなら、以下を満たすある\(\widetilde{s} \in \widetilde{S}\)、つまり、\(g (f (s)) = g (\widetilde{s})\)、がある、それが含意するのは、\(f (s) = \widetilde{s} \in \widetilde{S}\)、したがって、\(s \in f^{-1} (\widetilde{S})\)。
したがって、\(p \in Sat (f^{-1} (\widetilde{S}), \sim')\)。
したがって、\(f'^{-1} (g (\widetilde{S})) \subseteq Sat (f^{-1} (\widetilde{S}), \sim')\)。
ステップ2:
\(p \in Sat (f^{-1} (\widetilde{S}), \sim')\)を任意のものとしよう。
以下を満たすある\(s \in f^{-1} (\widetilde{S})\)、つまり、\(p \sim' s\)、がある、それが含意するのは、\(f' (p) = f' (s)\)。
\(f (s) \in \widetilde{S}\)。
\(g (f (s)) \in g (\widetilde{S})\)。
しかし、\(f' (p) = f' (s) = f' \vert_S (s) = g (f (s))\)、任意のセット（集合）で任意のイクイバレンスリレーション（同値関係）を持つものおよび任意のサブセット（部分集合）で当該サブセット（部分集合）イクイバレンスリレーション（同値関係）を持つものに対して、当該サブセット（部分集合）のクオシエント（商）セット（集合）から当該セット（集合）のクオシエント（商）セット（集合）の中へのカノニカル（正典）インジェクション（単射）があるという命題によって、\(\in g (\widetilde{S})\)。
したがって、\(p \in f'^{-1} (g (\widetilde{S}))\)。
したがって、\(Sat (f^{-1} (\widetilde{S}), \sim') \subseteq f'^{-1} (g (\widetilde{S}))\)。
ステップ3:
したがって、\(f'^{-1} (g (\widetilde{S})) = Sat (f^{-1} (\widetilde{S}), \sim')\)。
