Proof of A Lipschitz Map is Uniformly Continuous and Continuous

By Lipschitz Map Between Metric Spaces §lipschitz, fix a real $L\ge0$ with $d_{Y}(f(x),f(x'))\le L\,d_{X}(x,x')$ for all $x,x'\in X$.

Clause uniformly-continuous. Let $\varepsilon>0$ be real. By Rules of Arithmetic and Order in an Ordered Field §squares, $0<1$, so $0<L+1$ by Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares §strict-sum applied to $0<1$ and $0\le L$; hence $L+1\neq0$ by Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders §strict-characterization, $0<(L+1)^{-1}$ by Rules of Arithmetic and Order in an Ordered Field §positive-reciprocal, and

$$\delta=\varepsilon\,(L+1)^{-1}$$

satisfies $0<\delta$ by Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares §positive-product; it depends on $\varepsilon$ and $L$ only. Let $x,x'\in X$ with $d_{X}(x,x')<\delta$. From $0<1$, Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders §weak-strict gives $0\le1$; from $L\le L$ and $0\le1$, Rules of Arithmetic and Order in an Ordered Field §order-sum gives $L\le L+1$; as $0\le d_{X}(x,x')$ by Metric Space §nonnegative, Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares §nonnegative-scaling gives $L\,d_{X}(x,x')\le(L+1)\,d_{X}(x,x')$. As $0<L+1$, Rules of Arithmetic and Order in an Ordered Field §order-product gives $(L+1)\,d_{X}(x,x')<(L+1)\,\delta=\varepsilon$. Hence

$$d_{Y}(f(x),f(x'))\le L\,d_{X}(x,x')\le(L+1)\,d_{X}(x,x')<\varepsilon,$$

so $d_{Y}(f(x),f(x'))<\varepsilon$ by transitivity of $\le$ and Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares §mixed. As $\varepsilon$ was arbitrary, $f$ is uniformly continuous by Uniformly Continuous Map Between Metric Spaces §uniformly-continuous, with $A=X$.

Clause continuous. By the clause uniformly-continuous, $f$ is uniformly continuous on $X$, so it is continuous on $X$, that is, continuous, by A Uniformly Continuous Map Between Metric Spaces Is Continuous §continuous with $A=X$.