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