A Compact Subset of a Metric Space as a Metric Space: Compactness, Local Compactness, Separability, Continuous Functions and Finite Borel Measures

In the setting of Measurable Functions and the Lebesgue Integral: Standing Notation and Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity, let $(S,d)$ be a metric space with Borel $\sigma$-algebra $\mathcal{B}(S)$, and let $K\subseteq S$ be compact in $(S,\mathcal{T}_{d})$. Let $d_{K}=d|_{K\times K}$ be the restricted metric (Subsets of a Metric Space: the Restricted Metric, Sequences, Limits in Closed Subsets and Completeness of Closed Subsets (i)), $\mathcal{T}_{d_{K}}$ its topology, $\mathcal{B}(K)$ the Borel $\sigma$-algebra of $(K,d_{K})$, and $\iota:K\to S$ the inclusion, $\iota(x)=x$.

(i) Compactness. The topological space $(K,\mathcal{T}_{d_{K}})$ is compact.

(ii) Local compactness. $(K,d_{K})$ is locally compact.

(iii) Separability. $(K,d_{K})$ is separable.

(iv) Continuous functions. Every continuous function $g:K\to\mathbb{R}$ on $(K,d_{K})$ has compact support. For every continuous function $f:S\to\mathbb{R}$, the restriction $f|_{K}=f\circ\iota$ is continuous on $(K,d_{K})$.

(v) Borel sets. $K\in\mathcal{B}(S)$, the inclusion $\iota$ is $\mathcal{B}(K)/\mathcal{B}(S)$-measurable, and

$$\mathcal{B}(K)=\{B\in\mathcal{B}(S):B\subseteq K\}.$$

(vi) Restriction of a measure. Let $\mu$ be a finite measure on $(S,\mathcal{B}(S))$, and let $\mu_{K}$ be its restriction to $\mathcal{B}(K)$. Then $\mu_{K}$ is a finite measure on $(K,\mathcal{B}(K))$ with $\mu_{K}(K)=\mu(K)$, and for every bounded $\mathcal{B}(S)$-measurable function $f:S\to\mathbb{R}$

$$\int_{K}f|_{K}\,d\mu_{K}=\int_{S}f\,\mathbf{1}_{K}\,d\mu .$$

(vii) Extension of a measure. Let $\nu$ be a finite measure on $(K,\mathcal{B}(K))$. Then its image measure $\nu\circ\iota^{-1}$ is a finite measure on $(S,\mathcal{B}(S))$ with $(\nu\circ\iota^{-1})(B)=\nu(B\cap K)$ for every $B\in\mathcal{B}(S)$, and for every bounded $\mathcal{B}(S)$-measurable function $f:S\to\mathbb{R}$

$$\int_{S}f\,d(\nu\circ\iota^{-1})=\int_{K}f|_{K}\,d\nu .$$