Euclidean Points as Tuples of Real Numbers

Let $n$ be a natural number, let $[n]$ be the initial segment determined by $n$, and let $\mathbb{R}$ be the set of real numbers.

Euclidean space $\mathbb{R}^n$ is introduced there as the set of all ordered $n$-tuples $(x_1,\dots,x_n)$ with each $x_i\in\mathbb{R}$, the term ordered $n$-tuple being left unanalysed. Throughout this item, and in any later item that cites it, we read that term by the definition of tuples in a set applied to the set $\mathbb{R}$: an ordered $n$-tuple of real numbers is a map from $[n]$ to $\mathbb{R}$; for $k\in[n]$ its value at $k$ is written $x_k$ and called the $k$-th component; and the display $(x_1,\dots,x_n)$ names such a map through its components. With this reading the set $\mathbb{R}^n$ of the Euclidean-space definition is the set $\mathbb{R}^n$ of the tuple definition, and the two notations agree.

We use the ambient conventions for maps: a map assigns to each element of its domain exactly one value, and two maps with the same domain are equal exactly when their values agree at every element of that domain.

Then the following hold.

1. (Extensionality.) Let $x,y\in\mathbb{R}^n$. Then $x=y$ if and only if $x_k=y_k$ for every $k\in[n]$.

2. (Prescribing components.) Suppose that to each $k\in[n]$ a real number $a_k$ is assigned. Then there is exactly one $x\in\mathbb{R}^n$ with $x_k=a_k$ for every $k\in[n]$.

3. (Maps with values in $\mathbb{R}^n$.) Let $S$ be a set. If for each $k\in[n]$ a map $f^k:S\to\mathbb{R}$ is given, then there is exactly one map $f:S\to\mathbb{R}^n$ such that $(f(s))_k=f^k(s)$ for every $s\in S$ and every $k\in[n]$. Conversely, if $f:S\to\mathbb{R}^n$ is a map and for each $k\in[n]$ the map $f^k:S\to\mathbb{R}$ is defined by $f^k(s)=(f(s))_k$, then $f$ is the unique map determined by $f^1,\dots,f^n$ in this way.