ThmDex – An index of mathematical definitions, results, and conjectures.
F8070
Formulation 0
The standard real exponentiation function with exponent $p \in \mathbb{R}$ is the D4364: Real function \begin{equation} \begin{cases} \mathbb{R} \setminus \{ 0 \} \to \mathbb{R}, \quad & x \mapsto x^p, \qquad \text{ if } p < 0 \\ \mathbb{R} \to \mathbb{R}, \quad & x \mapsto x^p, \qquad \text{ if } p \geq 0 \\ \end{cases} \end{equation}