ThmDex – An index of mathematical definitions, results, and conjectures.
Formulation 1
Let $\mathbb{R}^N$ and $\mathbb{R}^M$ each 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 of $X$ in $\mathbb{R}^N$
(iv) $\mathcal{L} = \mathcal{L}(\mathbb{R}^N \to \mathbb{R}^M)$ is the D3208: Set of linear functions from $\mathbb{R}^N$ to $\mathbb{R}^M$ over $\mathbb{R}$
(v) $\Vert \cdot \Vert_2$ is a D1383: Euclidean length function on $\mathbb{R}^N$
A D4363: Euclidean real function $f : X \to \mathbb{R}^M$ 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{\Vert f(x) - f(x_0) - L(x - x_0) \Vert_2}{\Vert x - x_0 \Vert_2} = 0 \end{equation}