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
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}
Also known as
Totally differentiable euclidean real function, Classically differentiable euclidean real function, Strongly differentiable euclidean real function
Children
▶ D1587: Euclidean real function slope
Results
▶ R2876: Real mean value inequality
▶ R3941: Slope function for standard real gaussian density function