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 ▼ Differentiable euclidean real function ▼ Strongly differentiable complex function
Definition D5614
Differentiable real function

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) $$X \neq \emptyset$$ (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 $$\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$$