Square root function

Definition

For a real number $x \ge 0$, the square root $\sqrt{x}$ is the unique real number $y \ge 0$ with $y^2 = x$. The square root function is the function $x \mapsto \sqrt{x}$ on $[0, \infty)$.

Remarks

The number $y$ exists by the intermediate value theorem for $t \mapsto t^2$. It is unique because $t^2$ is strictly increasing on $[0, \infty)$. The function is continuous and strictly increasing. It is differentiable on $(0, \infty)$, but not at $0$. For $x > 0$, $\sqrt{x} = x^{1/2}$. Also $\sqrt{x^2} = |x|$ for every real $x$. Mathlib defines Real.sqrt, with $\sqrt{x} = 0$ for $x < 0$.

Explanations

L1 human

The square root of $x$ is the nonnegative number whose square is $x$. For example, $\sqrt{9} = 3$, not $-3$.