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}
Children
Euclidean real function slope
Results
Real mean value inequality
Slope function for standard real gaussian density function