ThmDex – An index of mathematical definitions, results, and conjectures.
Result R4542 on D216: Inverse map
Map is inverse to its inverse
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$ is an D216: Inverse map for $f^{-1}$.
Subresults
R4543: Map inverse is invertible
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$
Clear from the definition.