description/proof of that inverse of bijection is bijection
Topics
About: set
The table of contents of this article
Starting Context
- The reader knows a definition of bijection.
- The reader knows a definition of inverse of map.
- The reader admits the proposition that any map is a bijection if and only if it has an inverse.
- The reader admits the proposition that for any map, if an inverse exists, the inverse is the unique inverse.
Target Context
- The reader will have a description and a proof of the proposition that the inverse of any bijection is a bijection.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description
Here is the rules of Structured Description.
Entities:
\(S_1\): \(\in \{\text{ the sets }\}\)
\(S_2\): \(\in \{\text{ the sets }\}\)
\(f\): \(: S_1 \to S_2\), \(\in \{\text{ the bijections }\}\)
//
Statements:
\(f^{- 1}: S_2 \in S_1 \in \{\text{ the bijections }\}\)
//
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.
