インフィニット（無限）セット（集合）に対して、もしも、セット（集合）からナチュラルナンバー（自然数）たちセット（集合）の中へのインジェクション（単射）がある場合、ナチュラルナンバー（自然数）たちセット（集合）からセット（集合）の上へのバイジェクション（全単射）があることの記述/証明
話題
About: セット（集合）
この記事の目次
開始コンテキスト
ターゲットコンテキスト
- 読者は、任意のインフィニット（無限）セット（集合）に対して、もしも、当該セット（集合）からナチュラルナンバー（自然数）たちセット（集合）の中への任意のインジェクション（単射）がある場合、ナチュラルナンバー（自然数）たちセット（集合）から当該セット（集合）の上へのあるバイジェクション（全単射）があるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(S\): \(\in \{\text{ 全てのインフィニット（無限）セット（集合）たち }\}\)
//
ステートメント（言明）たち:
\(\exists f: S \to \mathbb{N} \in \{\text{ 全てのインジェクション（単射）たち }\}\)
\(\implies\)
\(\exists f'': \mathbb{N} \to S \in \{\text{ 全てのバイジェクション（全単射）たち }\}\)
//
2: 注
したがって、\(S\)はカウンタブル（可算）である。
3: 証明
全体戦略: ステップ1: バイジェクション（全単射）\(f^`: S \to f (S)\)およびそのインバース（逆）\({f^`}^{-1}: f (S) \to S\)を得る; ステップ2: 任意の\(s_0 \in S\)およびサージェクション（全射）\(f': \mathbb{N} \to S, n \mapsto {f^`}^{-1} (n) \text{ 、 } n \in f (S) \text{ である時 }; \mapsto s_0 \text{ 、その他の時 }\)を取る; ステップ3: 任意のインフィニットセット（無限集合）に対して、もしも、ナチュラルナンバー（自然数）たちセット（集合）から当該セット（集合）の上へのあるサージェクション（全射）がある場合、ナチュラルナンバー（自然数）たちセット（集合）から当該セット（集合）の上へのあるバイジェクション（全単射）があるという命題を適用する。
ステップ1:
\(f\)のコドメイン（余域）リストリクション（制限）\(f^`: S \to f (S), s \mapsto f (s)\)はあるバイジェクション（全単射）である。
\(f^`\)のインバース（逆）\({f^`}^{-1}: f (S) \to S\)がある。
ステップ2:
\(s_0 \in S\)を任意のものとしよう、それは、存在する、なぜなら、\(S \neq \emptyset\)。
\(f': \mathbb{N} \to S, n \mapsto {f^`}^{-1} (n) \text{ 、 } n \in f (S)\text{ である時 }; \mapsto s_0 \text{ 、そうでない時 }\)を定義しよう。
\(f'\)はあるサージェクション（全射）である、なぜなら、各\(s \in S\)に対して、\(f (s) \in f (S)\)、したがって、\(f' (f (s)) = {f^`}^{-1} (f (s)) = {f^`}^{-1} (f^` (s)) = s\)。
ステップ3:
あるバイジェクション（全単射）\(f'': \mathbb{N} \to S\)がある、任意のインフィニットセット（無限集合）に対して、もしも、ナチュラルナンバー（自然数）たちセット（集合）から当該セット（集合）の上へのあるサージェクション（全射）がある場合、ナチュラルナンバー（自然数）たちセット（集合）から当該セット（集合）の上へのあるバイジェクション（全単射）があるという命題によって。
