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
▼ Indexed sum
▼ Series
▼ Power series
▼ Convergent power series
▼ Convergent basic real power series
Definition D1932
Standard natural real exponential function
Formulation 0
The standard natural real exponential function is the D5482: Positive real function \begin{equation} \mathbb{R} \to (0, \infty), \quad x \mapsto \lim_{N \to \infty} \sum_{n = 0}^N \frac{x^n}{n!} \end{equation}
Formulation 1
The standard natural real exponential function is the D5482: Positive real function \begin{equation} \mathbb{R} \to (0, \infty), \quad x \mapsto \frac{x^0}{0!} + \frac{x^1}{1!} + \frac{x^2}{2!} + \frac{x^3}{3!} + \frac{x^4}{4!} + \frac{x^5}{5!} + \frac{x^6}{6!} + \dots \end{equation}
Formulation 2
The standard natural real exponential function is the D5482: Positive real function \begin{equation} \mathbb{R} \to (0, \infty), \quad x \mapsto \sum_{n = 0}^{\infty} \frac{x^n}{n!} \end{equation}
Children
▶ D169: Napier's constant
▶ D5752: Softmax function
Results
▶ R4900
▶ R4873
▶ R4673: Napier's constant equals a limit of products with factors nearing one
▶ R3385: Standard approximating sequence for the natural exponential function
▶ R4285: Standard natural real exponential function maps zero to one
Conventions
▶
Convention 0 (Notation for standard natural basic real exponential function)
The notation used for the D1932: Standard natural real exponential function is $x \mapsto \exp(x)$. Due to result R3621: Standard natural exponential function equals powers of Napier's constant, one may also use $x \mapsto e^x$.