Restriction of Real Square Mapping to Positive Reals is Bijection

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $f: \R \to \R$ be the real square function:

$\forall x \in \R: \map f x = x^2$

Let $g: \R_{\ge 0} \to R_{\ge 0} := f {\restriction_{\R_{\ge 0} \times R_{\ge 0} } }$ be the restriction of $f$ to the positive real numbers $\R_{\ge 0}$.


Then $g$ is a bijective restriction of $f$.


Proof

From Order is Preserved on Positive Reals by Squaring, $f$ is strictly increasing on $\R_{\ge 0}$.

By definition, a strictly increasing real function is strictly monotone.

The result follows from Strictly Monotone Real Function is Bijective.

$\blacksquare$


Sources