ThmDex – An index of mathematical definitions, results, and conjectures.
Result R4543 on D216: Inverse map
Map inverse is invertible
Formulation 0
Let $f : X \to Y$ be a D18: Map such that
(i) $f^{-1} : Y \to X$ is an D216: Inverse map for $f$
Then $f^{-1}$ is an D976: Invertible map.
Proofs
Proof 0
Let $f : X \to Y$ be a D18: Map such that
(i) $f^{-1} : Y \to X$ is an D216: Inverse map for $f$
This result is a particular case of R4542: Map is inverse to its inverse. $\square$