マップ（写像）はバイジェクション（全単射）である、もしも、それは、インバース（逆）を持つ場合、そして、その場合に限って、ことの記述/証明
話題
About: セット（集合）
この記事の目次
開始コンテキスト
- 読者は、バイジェクション（全単射）の定義を知っている。
- 読者は、マップ（写像）のインバース（逆）の定義を知っている。
ターゲットコンテキスト
- 読者は、任意のマップ（写像）はあるバイジェクション（全単射）である、もしも、それは、あるインバース（逆）を持つ場合、そして、その場合に限って、という命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(S_1\): \(\in \{\text{ 全てのセット（集合）たち }\}\)
\(S_2\): \(\in \{\text{ 全てのセット（集合）たち }\}\)
\(f\): \(: S_1 \to S_2\)
//
ステートメント（言明）たち:
\(f \in \{\text{ 全てのバイジェクション（全単射）たち }\}\)
\(\iff\)
\(\exists f^{- 1}: S_2 \to S_1 \in \{f \text{ の全てのインバース（逆）たち } \}\)
//
2: 注
実のところ、もしも、ある\(f^{- 1}\)が存在する場合、\(f^{- 1}\)がユニークインバース（逆）である、任意のマップ（写像）に対して、もしも、あるインバース（逆）が存在する場合、当該インバース（逆）がユニークインバース（逆）であるという命題.
3: Proof
Whole Strategy: Step 1: suppose that \(f\) is a bijection; Step 2: construct an \(f^{- 1}\); Step 3: suppose that \(f\) has an \(f^{- 1}\); Step 4: see that \(f\) is a bijections.
Step 1:
Let us suppose that \(f\) is a bijection.
Step 2:
Let us construct the \(f^{- 1}: S_2 \to S_1\) as this: for each \(s_2 \in S_2\), as \(f\) is a surjection, there is an \(s_1 \in S_1\) such that \(f (s_1) = s_2\), but as \(f\) is an injection, there is only \(1\) such an \(s_1 \in S_1\), so, let \(f^{- 1} (s_2) = s_1\).
\(f^{- 1} \circ f = id_{S_1}\), because for each \(s_1 \in S_1\), \(f^{- 1} \circ f (s_1) = s_1\), because \(f^{- 1} (f (s_1))\) is \(s'_1 \in S_1\) such that \(f (s'_1) = f (s_1)\), which implies that \(s'_1 = s_1\).
\(f \circ f^{- 1} = id_{S_2}\), because for each \(s_2 \in S_2\), \(f \circ f^{- 1} (s_2) = s_2\), because \(f^{- 1} (s_2)\) is \(s'_1 \in S_1\) such that \(f (s'_1) = s_2\), so, \(f \circ f^{- 1} (s_2) = f (s'_1) = s_2\).
So, \(f^{- 1}\) is an inverse of \(f\), in fact, \(f^{- 1}\) is the inverse of \(f\).
Step 3:
Let us suppose that \(f\) has an inverse, \(f^{- 1}: S_2 \to S_1\).
\(f\) is an injection, because otherwise, there would be some \(s_1, s'_1 \in S_1\) such that \(s_1 \neq s'_1\) and \(f (s_1) = f (s'_1)\), but \(s_1 = id_{S_1} (s_1) = f^{- 1} \circ f (s_1) = f^{- 1} \circ f (s'_1) = id_{S_1} (s'_1) = s'_1\), a contradiction against \(s_1 \neq s'_1\).
\(f\) is a surjection, because otherwise, there would an \(s_2 \in S_2\) that was not mapped to by \(f\), but \(s_2 = id_{S_2} (s_2) = f \circ f^{- 1} (s_2) = f (f^{- 1} (s_2))\), so, \(f^{- 1} (s_2) \in S_1\) would be mapped to \(s_2\), a contradiction against that \(s_2\) is not mapped to by \(f\).
So, \(f\) is a bijection.
