ThmDex – An index of mathematical definitions, results, and conjectures.

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.