ThmDex – An index of mathematical definitions, results, and conjectures.

Result R4906 on D5681: Real function derivative
Subresult of R4903: Strong derivative for affine basic real function

Formulation 0

Let $f : \mathbb{R}^N \to \mathbb{R}$ be a D4364: Real function such that

(i)	\begin{equation} \exists \, a, b \in \mathbb{R} : \forall \, x \in \mathbb{R}^N : f(x) = a x + b \end{equation}

Let $L : \mathbb{R}^N \to \mathbb{R}$ be a D4364: Real function such that

(i)	\begin{equation} \forall \, x \in \mathbb{R}^N : L(x) = a x \end{equation}

Then $L$ is a D5681: Real function derivative for $f$ on $\mathbb{R}^N$.

Proofs

Proof 0

Let $f : \mathbb{R}^N \to \mathbb{R}$ be a D4364: Real function such that

(i)	\begin{equation} \exists \, a, b \in \mathbb{R} : \forall \, x \in \mathbb{R}^N : f(x) = a x + b \end{equation}

Let $L : \mathbb{R}^N \to \mathbb{R}$ be a D4364: Real function such that

(i)	\begin{equation} \forall \, x \in \mathbb{R}^N : L(x) = a x \end{equation}

This result is a particular case of R4903: Strong derivative for affine basic real function. $\square$