Local comparison of a riemannian metric with the euclidean metric

Given: A compact set $K$ in a single chart.

Coordinate criterion for a riemannian metric: A tensor $g={\sum }_{i,j}{g}_{ij}d{x}^i\otimes d{x}^j$ is Riemannian exactly when its coordinate matrix $G=(g_{ij})$ has smooth entries and is symmetric positive definite. Under $J=\mathrm{\partial }x\mathrm{/}\mathrm{\partial }y$ it transforms by $G_y=J^T{G}_{x}J$.

A product of finitely many compact spaces is compact in the product topology: For every $n\in \mathbb{N}$ (def-natural-numbers) and every family $(X_k{)}_{k<n}$ of compact topological spaces (def-compact-space, def-topological-space), the product ${\prod }_{k<n}{X}_k$ with the product topology (def-product-topology) is compact. In particular a binary product $X\times Y$ of compact spaces is compact, and the empty product, a one-point space, is compact. No choice principle is used beyond lem-finite-choice, which is a theorem of ZF. That is what separates the finite case from the arbitrary one, where the Axiom of Choice is genuinely spent.

A subset of ${\mathbb{R}}^n$ with the product topology is compact exactly when it is closed and bounded, the product topology being the Euclidean metric topology: Let $n\in \mathbb{N}$ with $n\ge 1$, let ${\mathbb{R}}^n$ be the set of functions $n\to \mathbb{R}$ (lem-metrics-on-rn) carrying the product topology of $n$ copies of the usual topology of $\mathbb{R}$ (def-product-topology), and let $d_2$ be the Euclidean metric. Then: 1. The product topology on ${\mathbb{R}}^n$ is the metric topology of $d_2$ (def-metric-topology), so ${\mathbb{R}}^n$ as a product and ${\mathbb{R}}^n$ as a metric space are one topological space, and it is metrizable (def-metrizable-space). 2. A subset $K\subseteq {\mathbb{R}}^n$ is a compact subset for the product topology (def-compact-space) if and only if $K$ is closed in ${\mathbb{R}}^n$ and bounded (def-metric-bounded-diameter). The hypothesis $n\ge 1$ is inherited from lem-metrics-on-rn, which defines ${\mathbb{R}}^n$ and its three metrics only there; for $n=0$ the product is a one-point space and is compact. No choice principle is used: the metric statement it is read off from is proved by bisection (thm-heine-borel-rn).

A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value: Let $(X,d)$ be a nonempty compact metric space (def-metric-compactness, def-metric-space) and let $f:X\to \mathbb{R}$ be continuous (def-metric-continuity), $\mathbb{R}$ carrying its usual metric $d_{\mathbb{R}}(s,t)=\mathrm{\mid }s-t\mathrm{\mid }$ (lem-real-line-is-a-metric-space). Then the image $f[X]$ is bounded above and below (def-bounded-set), and it has a maximum and a minimum (def-max-min): there are points $x_{\max },x_{\min }\in X$ with $f(x_{\min })\le f(x)\le f(x_{\max })\text{for every }x\in X,$ and then $f(x_{\max })=\sup f[X]$ and $f(x_{\min })=\inf f[X]$ (def-complete-ordered-field, def-infimum). Nonemptiness of $X$ is a hypothesis and not an oversight: for $X=\mathrm{\varnothing }$ the image is empty and has neither a supremum nor a maximum. No choice principle is used.

For a metric space with its metric topology, compactness in the topological sense is compactness in the metric sense, and the two notions of compact subset coincide: Let $(X,d)$ be a metric space (def-metric-space) and let ${\mathcal{T}}_d$ be its metric topology (def-metric-topology), so that $(X,{\mathcal{T}}_d)$ is a topological space (def-topological-space) and is metrizable (def-metrizable-space). Then: 1. $(X,d)$ is a compact metric space (def-metric-compactness) if and only if $(X,{\mathcal{T}}_d)$ is a compact topological space (def-compact-space). 2. For every $A\subseteq X$: $A$ is a compact subset of the metric space $(X,d)$ if and only if $A$ is a compact subset of the topological space $(X,{\mathcal{T}}_d)$, the two readings of "compact subset" being the metric subspace $(A,d_A)$ (def-isometry-and-metric-embedding) and the topological subspace $(A,({\mathcal{T}}_d{)}_A)$ (def-subspace-topology-top). Nothing here is a coincidence and nothing is transported. The open-cover condition of def-metric-compactness quantifies over families of subsets open in $(X,d)$, and by def-metric-topology those are exactly the members of ${\mathcal{T}}_d$; so the two conditions are not merely equivalent, they are the same condition written twice. No choice principle is used.