Solution (source code)

= Solution

A <function> $f:A\to B$ is \b[onto], or a <surjective function>, when every $b\in B$ has a preimage: $\forall b\in B\ \exists a\in A:\ f(a)=b$. It is \b[one-to-one], or an <injective function>, when $f(a)=f(a')$ implies $a=a'$ for all $a,a'\in A$. It is \b[bijective], a <bijection>, when both properties hold.

An <inverse function> is a <function> $f^{-1}:B\to A$ satisfying
$$
\boxed{f^{-1}\circ f=\operatorname{id}_A,\qquad f\circ f^{-1}=\operatorname{id}_B}.
$$
For a <bijection>, $f^{-1}(b)$ is the unique $a$ with $f(a)=b$: existence follows from <surjectivity> and uniqueness from <injectivity>. This is a two-sided <inverse function>, rather than just a left or right inverse.