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