The Weighted Uniform Distance Is a Metric, and Is Complete When the Target Is Complete

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $a,b\in\mathbb{R}$ with $a<b$, with the closed interval $[a,b]$, let $(Y,d_{Y})$ be a metric space, and let $w:[a,b]\to\mathbb{R}$ be a map continuous on $[a,b]$ with $w(t)>0$ for every $t\in[a,b]$, where $[a,b]$ carries the distance $d_{\mathbb{R}}$ of Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces (iv). Let $C([a,b],Y)$ be the set of maps $[a,b]\to Y$ continuous on $[a,b]$ of The Space of Continuous Maps on a Closed Interval and Its Weighted Uniform Distance (i), and $d_{w}$ the weighted uniform distance on it.

(i) $d_{w}$ is a metric on $C([a,b],Y)$, so that $(C([a,b],Y),d_{w})$ is a metric space.

(ii) If $Y$ is nonempty, then $C([a,b],Y)$ is nonempty: for every $c\in Y$, the constant map $[a,b]\to Y$ with value $c$ lies in $C([a,b],Y)$.

(iii) If $(Y,d_{Y})$ is complete, then $(C([a,b],Y),d_{w})$ is complete.