パーミュテーション（並べ替え）は、パーミュテーション（並べ替え）たちのセット（集合）をパーミュテーション（並べ替え）たちのセット（集合）の上へバイジェクティブ（全単射）にマップする、左または右からコンポジション（合成）によって、ことの記述/証明
話題
About: セット（集合）
この記事の目次
開始コンテキスト
ターゲットコンテキスト
- 読者は、任意のパーミュテーション（並べ替え）は、全てのパーミュテーション（並べ替え）たちのセット（集合）を全てのパーミュテーション（並べ替え）たちのセット（集合）の上へバイジェクティブ（全単射）にマップする、左または右からコンポジション（合成）によって、という命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(S\): \(\subseteq \mathbb{N}\)
\(f\): \(\in \{S \text{ 上方の全てのシーケンス（列）たち }\}\)
\(P\): \(= \{f \text{ の全てのパーミュテーション（並べ替え）たち }\}\)
\(\sigma_0\): \(\in P\)
\(l_{\sigma_0}\): \(P \to P, \sigma \mapsto \sigma_0 \circ \sigma\)
\(r_{\sigma_0}\): \(P \to P, \sigma \mapsto \sigma \circ \sigma_0\)
//
ステートメント（言明）たち:
\(l_{\sigma_0} \in \{\text{ 全てのバイジェクション（全単射）たち }\}\).
\(\land\)
\(r_{\sigma_0} \in \{\text{ 全てのバイジェクション（全単射）たち }\}\).
//
2: 自然言語記述
任意のサブセット（部分集合）\(S \subseteq \mathbb{N}\)、以下を満たす任意のシーケンス（列）\(f\)、つまり、\(dom f = S\)、\(f\)の全てのパーミュテーション（並べ替え）たちのセット（集合）\(P\)、任意のパーミュテーション（並べ替え）\(\sigma_0 \in P\)、\(l_{\sigma_0}\): \(P \to P, \sigma \mapsto \sigma_0 \circ \sigma\)、\(r_{\sigma_0}\): \(P \to P, \sigma \mapsto \sigma \circ \sigma_0\)に対して、\(l_{\sigma_0}\)および\(r_{\sigma_0}\)はバイジェクション（全単射）たちである。
3: 証明
全体戦略: ステップ1: \(l_{\sigma_0}\)および\(r_{\sigma_0}\)はウェルデファインド（妥当に定義された）であることを見る; ステップ2: \({\sigma_0}^{-1} \in P\)を取る; ステップ3: \(l_{\sigma_0}\)はバイジェクティブ（全単射）であることを見る、\({\sigma_0}^{-1}\)を使って; ステップ4: \(r_{\sigma_0}\)はバイジェクティブ（全単射）であることを見る、\({\sigma_0}^{-1}\)を使って。
ステップ1:
\(l_{\sigma_0}\)および\(r_{\sigma_0}\)はウェルデファインド（妥当に定義されている）（コドメイン（余域）は本当に\(P\)である）である、なぜなら、任意の2バイジェクション（全単射）のコンポジション（合成）で第1のバイジェクション（全単射）のコドメイン（余域）が第2のバイジェクション（余域）のドメイン（定義域）に等しいものはバイジェクション（全単射）である、バイジェクション（全単射）たちの任意のファイナイト（有限）コンポジション（合成）はバイジェクション（全単射）である、もしも、構成要素バイジェクション（全単射）たちのコドメイン（余域）たちが、引き続くバイジェクション（全単射）たちのドメイン（定義域）たちに等しい場合、という命題によって。
ステップ2:
\(\sigma_0\)の以下を満たすインバース（逆）\({\sigma_0}^{-1} \in P\)、つまり、\({\sigma_0}^{-1} \circ \sigma_0 = \sigma_0 \circ {\sigma_0}^{-1} = id\)、がある、なぜなら、\(\sigma_0\)はバイジェクション（全単射）であり、\({\sigma_0}^{-1}\)もバイジェクション（全単射）である。
ステップ3:
\(l_{\sigma_0}\)はインジェクション（単射）であることを証明しよう。
\(\sigma \neq \sigma' \in P\)は任意のパーミュテーション（並べ替え）たちであるとしよう。\(\sigma_0 \circ \sigma = \sigma_0 \circ \sigma'\)であると仮定しよう。\(\sigma = {\sigma_0}^{-1} \circ \sigma_0 \circ \sigma = {\sigma_0}^{-1} \circ \sigma_0 \circ \sigma' = \sigma'\)、矛盾。したがって、\(\sigma_0 \circ \sigma \neq \sigma_0 \circ \sigma'\)。
\(l_{\sigma_0}\)はサージェクション（全射）であることを証明しよう。
\(\sigma' \in P\)は任意のパーミュテーション（並べ替え）であるとしよう。\({\sigma_0}^{-1} \circ \sigma' \in P\)および\(\sigma_0 \circ {\sigma_0}^{-1} \circ \sigma' = \sigma'\)。
ステップ4:
\(r_{\sigma_0}\)はインジェクション（単射）であることを証明しよう。
\(\sigma \neq \sigma' \in P\)は任意のパーミュテーション（並べ替え）たちであるとしよう。\(\sigma \circ \sigma_0 = \sigma' \circ \sigma_0\)であると仮定しよう。\(\sigma = \sigma \circ \sigma_0 \circ {\sigma_0}^{-1} = \sigma' \circ \sigma_0 \circ {\sigma_0}^{-1} = \sigma'\)、矛盾。したがって、\(\sigma \circ \sigma_0 \neq \sigma' \circ \sigma_0\)。
\(r_{\sigma_0}\)はサージェクション（全射）であることを証明しよう。
\(\sigma' \in P\)は任意のパーミュテーション（並べ替え）であるとしよう。\(\sigma' \circ {\sigma_0}^{-1} \in P\)および\(\sigma' \circ {\sigma_0}^{-1} \circ \sigma_0 = \sigma'\)。
