ThmDex – An index of mathematical definitions, results, and conjectures.
Set of symbols
Alphabet
Deduction system
Theory
Zermelo-Fraenkel set theory
Set
Binary cartesian set product
Binary relation
Map
Operation
N-operation
Binary operation
Enclosed binary operation
Groupoid
Semigroup
Standard N-operation
Exponentiation
Root
Real root
Rational exponentiation
Real exponentiation
Definition D2410
Standard real exponentiation function
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}
Children
Real square function