インジェクション（単射）たちのファイナイト（有限）コンポジション（合成）はインジェクション（単射）であることの記述/証明
話題
About: セット（集合）
この記事の目次
開始コンテキスト
- 読者は、インジェクション（単射）の定義を知っている。
ターゲットコンテキスト
- 読者は、インジェクション（単射）たちの任意のファイナイト（有限）コンポジション（合成）はインジェクション（単射）であるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(\{S_1, ..., S_n\}\): \(S_j \in \{\text{ 全てのセット（集合）たち }\}\)
\(\{S'_1, ..., S'_n\}\): \(S'_j \in \{\text{ 全てのセット（集合）たち }\}\)
\(\{f_1, ..., f_n\}\): \(f_j: S_j \to S'_j\), \(\in \{\text{ 全てのインジェクション（単射）たち }\}\)
//
ステートメント（言明）たち:
\(\forall j \in \{1, ..., n - 1\} (S'_j \subseteq S_{j + 1})\)
\(\implies\)
\(f_n \circ ... \circ f_1: S_1 \to S'_n \in \{\text{ 全てのインジェクション（単射）たち }\}\)
//
2: 自然言語記述
任意のセット（集合）たち\(\{S_1, ..., S_n\}\)、任意のセット（集合）たち\(\{S'_1, ..., S'_n\}\)、以下を満たす任意のインジェクション（単射）たち\(\{f_1, ..., f_n\}\)、つまり、\(f_j: S_j \to S'_j\)、に対して、もしも、各\(j \in \{1, ..., n - 1\}\)に対して\(S'_j \subseteq S_{j + 1}\)である場合、\(f_n \circ ... \circ f_1: S_1 \to S'_n\)はインジェクション（単射）である。
3: 証明
全体戦略: それを\(n\)に関してインダクティブ（帰納的）に証明する; ステップ1: それを\(n = 1\)ケースに対して証明する; ステップ2: それを\(n = 2\)ケースに対して証明する; ステップ3: それを\(n = 1, ..., n' - 1\)ケースたちに対して仮定し、それを\(n = n'\)ケースに対して証明する。
それを\(n\)に関してインダクティブ（帰納的）に証明しよう。
ステップ1:
\(n = 1\)であると仮定しよう。
\(f_1\)はインジェクション（単射）である。
ステップ2:
\(n = 2\)であると仮定しよう。
\(p_1, p_2 \in S_1\)を、\(p_1 \neq p_2\)を満たす任意のものとしよう。\(f_1 (p_1) \neq f_1 (p_2)\)、\(f_1\)のインジェクティブ（単射）性によって。\(f_2 \circ f_1 (p_1) \neq f_2 \circ f_1 (p_2)\)、\(f_2\)のインジェクティブ（単射）性によって。したがって、\(f_2 \circ f_1\)はインジェクション（単射）である。
ステップ3:
本命題は\(n = 1, ..., n' - 1\)ケースたちに対して成立すると仮定しよう。
\(n = n'\)だと仮定しよう。
\(f_{n'} \circ ... \circ f_1 = f_{n'} \circ (f_{n' - 1} \circ ... \circ f_1)\)。\(f_{n' - 1} \circ ... \circ f_1\)はインジェクション（単射）である、\(n = n' - 1\)ケースに対するインダクション（帰納）仮定によって。\(f_{n'} \circ (f_{n' - 1} \circ ... \circ f_1)\)はインジェクション（単射）である、\(n = 2\)ケースに対する本命題によって。
4: 注
ステップ2を本当に私たちは必要とするのか？そう思う: ステップ2無しに\(f_{n'} \circ (f_{n' - 1} \circ ... \circ f_1)\)はインジェクション（単射）であると、本命題が\(n = 1, ..., n' - 1\)ケースたちに対して成立することのみを根拠に主張する誘惑にかられるかもしれないが、\(n' = 2\)である時、仮定されているのは、\(n = 1 = n' - 1\)ケースだけだ。
