ThmDex – An index of mathematical definitions, results, and conjectures.
Result R2962 on D4659: Natural real exponential function
Subresult of R5197: Characterisation of natural real exponential function by a differential equation
Characterisation of standard natural real exponential function by a differential equation
Formulation 0
Let $f : \mathbb{R} \to (0, \infty)$ be a D5614: Differentiable real function.
Let $\exp : \mathbb{R} \to (0, \infty)$ be the D1932: Standard natural real exponential function.
Then $f = \exp$ if and only if
(1) $\forall \, x \in \mathbb{R}: f'(x) = f(x)$
(2) $f(0) = 1$
Proofs
Proof 0
Let $f : \mathbb{R} \to (0, \infty)$ be a D5614: Differentiable real function.
Let $\exp : \mathbb{R} \to (0, \infty)$ be the D1932: Standard natural real exponential function.