ThmDex – An index of mathematical definitions, results, and conjectures.
F11532
Formulation 0
Let $f : \mathbb{R}^N \to \mathbb{R}^M$ be a D4363: Euclidean real function such that
(i) \begin{equation} \exists \, C \in \mathbb{R}^M : \forall \, x \in \mathbb{R}^N : f(x) = C \end{equation}
Let $L : \mathbb{R}^N \to \mathbb{R}^M$ be a D4364: Real function such that
(i) \begin{equation} \forall \, x \in \mathbb{R}^N : L(x) = (0, 0, \ldots, 0) \end{equation}
Then $L$ is a D111: Euclidean real function derivative for $f$ on $\mathbb{R}^N$.