Let $f : X \to Y$ be a D216: Inverse map such that

(i) | $f^{-1} : Y \to X$ is an D216: Inverse map of $f$ |

Then $f^{-1}$ is a D468: Bijective map.

Result R4540
on D468: Bijective map

Inverse map is a bijection

Formulation 0

Let $f : X \to Y$ be a D216: Inverse map such that

(i) | $f^{-1} : Y \to X$ is an D216: Inverse map of $f$ |

Then $f^{-1}$ is a D468: Bijective map.

Proofs

Let $f : X \to Y$ be a D216: Inverse map such that

(i) | $f^{-1} : Y \to X$ is an D216: Inverse map of $f$ |

Result R4543: Map inverse is invertible shows that $f^{-1}$ is an invertible map and result R1478: Equivalent characterisations of bijectivity shows that a map is a bijection if and only if it is an invertible map. $\square$