(i) | $|\cdot|$ is the D1383: Euclidean length function on $\mathbb{R}^D$ |
(ii) | $f : \mathbb{R}^D \to \mathbb{R}$ is a D4364: Real function on $\mathbb{R}^D$ |
(i) | $|\cdot|$ is the D1383: Euclidean length function on $\mathbb{R}^D$ |
(ii) | $f : \mathbb{R}^D \to \mathbb{R}$ is a D4364: Real function on $\mathbb{R}^D$ |