(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) | $f : X \to \mathbb{R}^M$ is a D1416: Differentiable euclidean real function at $x_0$ |
(v) | $\mathcal{L} : \mathbb{R}^N \to \mathbb{R}^M$ is a D111: Euclidean real function derivative for $f$ at $x_0$ |