[proofplan] We show that every exponent $s$ exceeding $\dim_{\mathcal{H}}(E)$ also exceeds $\dim_{\mathcal{H}}(f(E))$. By the definition of Hausdorff dimension, $s > \dim_{\mathcal{H}}(E)$ implies $\mathcal{H}^s(E) = 0$. The [Lipschitz Bound on Hausdorff Measure](/theorems/3056) then forces $\mathcal{H}^s(f(E)) = 0$, which in turn gives $\dim_{\mathcal{H}}(f(E)) \leq s$. Since $s$ was arbitrary, the result follows. [/proofplan] [step:Show $\mathcal{H}^s(f(E)) = 0$ for every $s > \dim_{\mathcal{H}}(E)$] Let $L = \operatorname{Lip}(f)$ denote the Lipschitz constant of $f$, and let $s > \dim_{\mathcal{H}}(E)$. By the definition of Hausdorff dimension, \begin{align*} \dim_{\mathcal{H}}(E) = \inf\{t \geq 0 : \mathcal{H}^t(E) = 0\}, \end{align*} so $s > \dim_{\mathcal{H}}(E)$ implies $\mathcal{H}^s(E) = 0$. Applying the [Lipschitz Bound on Hausdorff Measure](/theorems/3056) to $f$ with exponent $s$: \begin{align*} \mathcal{H}^s(f(E)) \leq L^s \, \mathcal{H}^s(E) = L^s \cdot 0 = 0. \end{align*} [/step] [step:Conclude $\dim_{\mathcal{H}}(f(E)) \leq \dim_{\mathcal{H}}(E)$ by taking the infimum] We have shown that $\mathcal{H}^s(f(E)) = 0$ for every $s > \dim_{\mathcal{H}}(E)$. By the definition of Hausdorff dimension applied to $f(E)$: \begin{align*} \dim_{\mathcal{H}}(f(E)) = \inf\{t \geq 0 : \mathcal{H}^t(f(E)) = 0\} \leq s \end{align*} for every $s > \dim_{\mathcal{H}}(E)$. Taking $s \to \dim_{\mathcal{H}}(E)^+$ yields \begin{align*} \dim_{\mathcal{H}}(f(E)) \leq \dim_{\mathcal{H}}(E). \end{align*} [/step]