インフィニットセット（無限集合）に対して、もしも、ナチュラルナンバー（自然数）たちセット（集合）からセット（集合）の上へのサージェクション（全射）がある場合、ナチュラルナンバー（自然数）たちセット（集合）からセット（集合）の上へのバイジェクション（全単射）があることの記述/証明
話題
About: セット（集合）
この記事の目次
開始コンテキスト
- 読者は、サージェクション（全射）の定義を知っている。
- 読者は、バイジェクション（全単射）の定義を知っている。
ターゲットコンテキスト
- 読者は、任意のインフィニットセット（無限集合）に対して、もしも、ナチュラルナンバー（自然数）たちセット（集合）から当該セット（集合）の上へのあるサージェクション（全射）がある場合、ナチュラルナンバー（自然数）たちセット（集合）から当該セット（集合）の上へのあるバイジェクション（全単射）があるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(S\): \(\in \{\text{ 全てのインフィニットセット（無限集合）たち }\}\)
//
ステートメント（言明）たち:
\(\exists f: \mathbb{N} \to S \in \{\text{ 全てのサージェクション（全射）たち }\}\)
\(\implies\)
\(\exists f': \mathbb{N} \to S \in \{\text{ 全てのバイジェクション（全単射）たち }\}\)
//
2: 注
当該ドメイン（定義域）が\(\mathbb{N}\)であることが、本命題のために決定的である。
もしも、当該ドメイン（定義域）が\(\mathbb{R}\)だったら、本命題は成立しないことになる: 例えば、\(S = \mathbb{Q}\)に対して、あるサージェクション（全射）\(f: \mathbb{R} \to \mathbb{Q}\)、例えば、\(f \vert_{\mathbb{Q}} = id\)および\(f \vert_{\mathbb{R} \setminus \mathbb{Q}} = 0\)、がある、しかし、バイジェクション（全単射）\(f': \mathbb{R} \to \mathbb{Q}\)は無い、よく知られているとおり。
3: 証明
全体戦略: ステップ1: インダクティブ（帰納的）に\(f'\)を定義し、\(f'\)はあるバイジェクション（全単射）であることを見る。
ステップ1:
\(f' (0) = f (0)\)としよう。
今や、私たちは、ペア\((f' \vert_{\{0\}}, n_0 := 0)\)、ここで、\(f' \vert_{\{0\}}\)はインジェクティブ（単射）であり、\(n_0\)は、\(\{f (0), ..., f (0)\}\)は既にカバーされたことを示す、を持っている。
\(1\)に対して、以下を満たす最小\(n_1 \in \mathbb{N}\)、つまり、\(n_0 \lt n_1\)および\(f (n_1) \notin \{f' (0)\}\)、を取ろう、それは、存在する、なぜなら、\(S\)はインフィニット（無限）である。
すると、\(f' (1) = f (n_1)\)としよう。
今や、私たちは、\((f' \vert_{\{0, 1\}}, n_1)\)、ここで、\(f' \vert_{\{0, 1\}}\)はインジェクティブ（単射）、を持っている。
\(2 \le n'\)に対して、私たちは、\((f' \vert_{\{0, ..., n' - 1\}}, n_{n' - 1})\)、ここで、\(f' \vert_{\{0, ..., n' - 1\}}\)はインジェクティブ（単射）、を持っていると仮定しよう。
\(n'\)に対して、以下を満たす最小\(n_{n'} \in \mathbb{N}\)、つまり、\(n_{n' - 1} \lt n_{n'}\)および\(f (n_{n'}) \notin \{f' (0), ..., f' (n' - 1)\}\)、を取ろう、それは、存在する、なぜなら、\(S\)はインフィニット（無限）である。
すると、\(f' (n') = f (n_{n'})\)としよう。
今や、私たちは、\((f' \vert_{\{0, .., n'\}}, n_{n'})\)、ここで、\(f' \vert_{\{0, ..., n'\}}\)はインジェクティブ（単射）、を持っている。
こうして、\(f'\)がインダクティブ（帰納的）に定義された。
\(f'\)はインジェクティブ（単射）である、なぜなら、以下を満たす各\(n, n' \in \mathbb{N}\)、つまり、\(n \lt n'\)、に対して、\(f' (n') \notin \{f' (0), ..., f' (n' - 1)\}\)、ここで、\(f' (n) \in \{f' (0), ..., f' (n' - 1)\}\)、それが意味するのは、\(f' (n) \neq f' (n')\)。
\(f'\)はサージェクティブ（全射）である、なぜなら、各\(s \in S\)に対して、\(n := Min (f^{-1} (s))\)としよう、すると、\(s = f (n)\)、そして、\(n_0 \lt n_1 \lt n_2 ...\)であるから、\(n \lt n_m\)、最小\(m\)に対して、すると、\(n_{m - 1} \le n\)、しかし、もしも、\(n_{m - 1} \lt n\)であったら、\(f (n) \notin \{f' (0) = f (0), ..., f' (m - 1) = f (n_{m - 1})\}\)、なぜなら、\(n = Min (f^{-1} (s))\)、それは、\(n_m\)はそうした最小\(n\)であったという事実に矛盾する、\(n \lt n_m\)であったところ、したがって、\(n_{m - 1} = n\)、したがって、\(f (n) = f (n_{m - 1}) = f' (m - 1)\)。
したがって、\(f'\)はあるバイジェクション（全単射）である。
