> [!NOTE] Theorem (Function is injective iff left-invertible) > Suppose $X$ and $Y$ are non-empty. Then $f:X\to Y$ is [[Injection|injective]] iff $f$ has a *[[Function Inverse|left inverse]]*. *Proof*. Suppose that $f$ is injective. Since $X$ is non-empty, fix some $x_{0}\in X.$ Now set $\left.g:Y\to X,y\mapsto\left\{\begin{array}{ll}x&\quad\mathrm{if~}\exists x:f(x)=y\\x_0&\quad\mathrm{otherwise}.\end{array}\right.\right. $Take any $x\in X.$ Set $y=f(x).$ Then $\begin{aligned} (g\circ f)(x)& =g(f(x)) && \text{definition of composition} \\ &=g(y)&& \text{definition of $y$} \\ &=x&& \text{first line of definition of }g \\ &=\mathrm{Id}_{X(x)}&&\text{definition of Id}_X \\ \end{aligned}$Hence $g \circ f = \text{Id}_{X},$ as required. Now suppose that $g$ is a left inverse for $f.$ Suppose that $f(x)=f(x').$ We now compute as follows: $ \begin{aligned} x & =\operatorname{Id}_X(x) & & \text { definition of } \operatorname{Id}_X \\ & =(g \circ f)(x) & & g \text { is a left inverse for } f \\ & =g(f(x)) & & \text { definition of composition } \\ & =g\left(f\left(x^{\prime}\right)\right) & & \text { since } f(x)=f\left(x^{\prime}\right) \\ & =(g \circ f)\left(x^{\prime}\right) & & \text { definition of composition } \\ & =\operatorname{Id}_X\left(x^{\prime}\right) & & g \text { is a left inverse for } f \\ & =x^{\prime} & & \text { definition of } \operatorname{Id}_X \end{aligned} $