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 ▼ Ringoid ▼ Semiring ▼ Ring ▼ Left ring action ▼ Module ▼ Linear combination ▼ Linear map ▼ Linear form ▼ Distribution ▼ Distributional derivative ▼ Weak derivative ▼ Real matrix function derivative ▼ Euclidean real function derivative
Definition D1416
Differentiable euclidean real function

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) $$X \neq \emptyset$$ (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 $$\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$$
Children
 ▶ D1587: Euclidean real function slope
Results
 ▶ R2876: Real mean value inequality ▶ R3941: Slope function for standard real gaussian density function