euclidean

Euclidean space

context	$n\in \mathbb N$
definiendum	$\mathbb E^n \equiv \langle d,\mathbb R^n\rangle$
inclusion	$d:\mathbb R^n\times \mathbb R^n\to \mathbb R_+$
postulate	$d(x,y):=\left( \sum_{j=1}^n (x_j-y_j)^2 \right)^\frac{1}{2}$