ThmDex – An index of mathematical definitions, results, and conjectures.
Formulation F10773 on D5614: Differentiable real function
F10773
Formulation 0
Let $\mathbb{R}^N$ be a D1512: Standard euclidean real norm-topological vector space such that
(i) $X \subseteq \mathbb{R}^N$ is a D5612: Euclidean real set
(ii) \begin{equation} X \neq \emptyset \end{equation}
(iii) $x_0 \in X$ is a D92: Limit point for $X$ in $\mathbb{R}^N$
(iv) $\mathcal{L} = \mathcal{L}(\mathbb{R}^N \to \mathbb{R})$ is the D3208: Set of linear functions from $\mathbb{R}^N$ to $\mathbb{R}$ over $\mathbb{R}$
A D4364: Real function $f : X \to \mathbb{R}$ is differentiable at $x_0$ if and only if \begin{equation} \exists \, L \in \mathcal{L} : \lim_{x \to x_0 ; \, x \in X \setminus \{ x_0 \}} \frac{|f(x) - f(x_0) - L(x - x_0)|}{|x - x_0|} = 0 \end{equation}