クオシエント（商）コレクションの定義
話題
About: コレクション
この記事の目次
開始コンテキスト
- 読者は、コレクション上のイクイバレンスリレーション（同値関係）の定義を知っている。
ターゲットコンテキスト
- 読者は、クオシエント（商）コレクションの定義を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\( C\): \(\in \{\text{ 全てのコレクションたち }\}\)
\( \sim\): \(\in \{C \text{ 上の全てのイクイバレンスリレーション（同値関係）たち }\}\)
\(*C / \sim\): \(= \{p \in Pow (C) \setminus \emptyset \vert \forall p', p'' \in p (p' \sim p'') \land \forall p' \in p, \forall p'' \in C \setminus p (\lnot p' \sim p'')\}\)
//
コンディションたち:
//
\(C / \sim\)は、ウェルデファイント（妥当に定義された）である、なぜなら、各\(p \in Pow (C) \setminus \emptyset\)に対して、\(p \in C / \sim\)か否かは曖昧でない。\(C / \sim\)は\(C\)をパーティション分けするかどうかは別の問題である、しかし、\(C / \sim\)は本当に\(C\)をパーティション化する、"注"内に示されているとおり。
言い換えると、クオシエント（商）コレクションは、\(C\)の\(\sim\)によるイクイバレンス（同値）クラスたちのコレクションである。
2: 注
\(C / \sim\)は\(C\)のあるパーティションである、それが意味するのは、\(C\)の各要素は\(C / \sim\)のある単一要素内に包含されていること: 各\(p \in C\)に対して、\(C / \sim\)の要素\([p]\)、\(\{p' \in C \vert p' \sim p\}\)によって定義された、がある、なぜなら、各\(p', p'' \in [p]\)に対して、\(p' \sim p\)および\(p'' \sim p\)、それが含意するのは、\(p' \sim p''\)、そして、各\(p' \in [p], p'' \in C \setminus [p]\)に対して、\(p \sim p'\)および\(\lnot p \sim p''\)、それが含意するのは、\(\lnot p' \sim p''\)、なぜなら、もしも、\(p' \sim p''\)であったら、\(p \sim p''\)、矛盾; \(p\)は\(C / \sim\)の他のどの要素にも所属しない、なぜなら、もしも、\(p\)は他の要素に所属していたら、\([p'] \in C / \sim\)、各要素\(p'' \in [p']\)に対して、\(p'' \sim p\)、それが意味することになるのは、\(p'' \in [p]\)、そして、各要素に対して、\(p'' \in [p]\)、\(p'' \sim p\)、それが意味することになるのは、\(p'' \in [p']\)、したがって、\([p'] = [p]\)、結局のところ。
\(f: C \to C / \sim, s \mapsto [s]\)は、"\(C\)の\(\sim\)に関するクラシフィケーションマップ（クラス分け写像）"と呼ばれる。
\(f\)はウェルデファイント（妥当に定義された）である、なぜなら、\([s] \in C / \sim\)はユニークに決定される、なぜなら、\(C / \sim\)は\(C\)のあるパーティションである。
\(f\)はあるサージェクション（全射）である、なぜなら、各\([s] \in C / \sim\)に対して、\(f (s) = [s]\)。
