ThmDex – An index of mathematical definitions, results, and conjectures.
Translation invariance of Euclidean volume function
Formulation 0
Let $\mathbb{R}^N$ be a D816: Euclidean real Cartesian product.
Let $\mathsf{Vol}$ be the D1738: Euclidean real volume function on $\mathbb{R}^N$.
Let $I \subseteq \mathbb{R}^N$ be D3036: Real N-interval.
Then \begin{equation} \forall \, x \in \mathbb{R}^N : \mathsf{Vol} (I + x) = \mathsf{Vol} (I) \end{equation}
Proofs
Proof 0
Let $\mathbb{R}^N$ be a D816: Euclidean real Cartesian product.
Let $\mathsf{Vol}$ be the D1738: Euclidean real volume function on $\mathbb{R}^N$.
Let $I \subseteq \mathbb{R}^N$ be D3036: Real N-interval.
Let $x \in \mathbb{R}^N$. By definition, $I$ is a Cartesian product of some basic real intervals $I_1, \dots, I_N$. Let $a_1, b_1, \dots, a_N, b_N$ be the endpoints of $I_1, \dots, I_N$, respectively. Result R2970: The four classes of real intervals are each closed under translation states that each interval $I_1, \dots, I_N$, when translated by $x_1, \dots, x_N$, respectively, is again a basic real interval with respective endpoints $a_1 + x_1, b_1 + x_1, \dots, a_N + x_N, b_N + x_N$. Applying R2968: Euclidean real Cartesian product of translations then yields \begin{equation} \begin{split} \mathsf{Vol}(I + x) & = \mathsf{Vol} \Big( \prod_{n = 1}^N (I_n + x_n) \Big) \\ & = \mathsf{Vol} \Big( \prod_{n = 1}^N |(b_n + x_n) - (a_n + x_n)| \Big) \\ & = \mathsf{Vol} \Big( \prod_{n = 1}^N |b_n - a_n| \Big) \\ & = \mathsf{Vol} \Big( \prod_{n = 1}^N I_n \Big) \\ & = \mathsf{Vol}(I) \end{split} \end{equation} Since $x \in \mathbb{R}^N$ was arbitrary, the claim follows. $\square$