ThmDex – An index of mathematical definitions, results, and conjectures.
Isotonicity of Euclidean volume function
Formulation 0
Let $\mathsf{P I} (\mathbb{R}^N)$ be a D1737: Set of real n-intervals.
Let $\mathsf{Vol}$ be the D1738: Euclidean real volume function on $\mathbb{R}^N$.
Then \begin{equation} \forall \, I, J \in \mathsf{P I} (\mathbb{R}^N) \, (I \subseteq J \quad \Rightarrow \quad \mathsf{Vol}(I) \leq \mathsf{Vol}(J)) \end{equation}
Proofs
Proof 0
Let $\mathsf{P I} (\mathbb{R}^N)$ be a D1737: Set of real n-intervals.
Let $\mathsf{Vol}$ be the D1738: Euclidean real volume function on $\mathbb{R}^N$.
Let $I$ and $J$ each be a Euclidean real interval such that $I \subseteq J$. By definition, each of $I$ and $J$ are finite Cartesian products of some basic real intervals $I^i_1, \dots, I^i_N$ and $I^j_1, \dots, I^j_N$, respectively. Denote the respective endpoints of these intervals as $a^i_1, b^i_1, \dots, a^i_N, b^i_N$ and $a^j_1, b^j_1, \dots, a^j_N, b^j_N$. Since $I$ is contained in $J$, then the inequality \begin{equation} |b^i_n - a^i_n| \leq |b^j_n - a^j_n| \end{equation} holds for every $1 \leq n \leq N$. Result R1937: Monotonicity of finite unsigned real multiplication now implies \begin{equation} \begin{split} \mathsf{Vol}(I) & = \mathsf{Vol} \Bigl( \prod_{n = 1}^N I^i_n \Bigr) \\ & = \prod_{n = 1}^N |b^i_n - a^i_n| \\ & \leq \prod_{n = 1}^N |b^j_n - a^j_n| \\ & = \mathsf{Vol} \Bigl( \prod_{n = 1}^N I^j_n \Bigr) \\ & = \mathsf{Vol}(J) \\ \end{split} \end{equation} $\square$