Whitney approximation for Euclidean-valued maps

If $M=\mathrm{\varnothing }$, the empty map proves the claim. Otherwise form the set of all tuples consisting of a smooth coordinate ball $B$, its chart data, and a point $x\in B$ such that $\bar{B}$ is compact and $\mathrm{\parallel }F(y)-F(x)\mathrm{\parallel }<\epsilon (y)\mathrm{/}2(y\in B)\mathrm{.}$ These balls cover $M$: for a fixed $x$, continuity gives a neighbourhood on which $\mathrm{\parallel }F(y)-F(x)\mathrm{\parallel }<\epsilon (x)\mathrm{/}4$ and $\epsilon (y)>\epsilon (x)\mathrm{/}2$, and [F2] supplies a smaller ball with compact closure. Fix a countable basis and use [A1] to choose one admissible tuple for each nonempty basis member contained in an eligible ball. Their balls cover $M$. Enumerate these tuples as $(B_n,x_n)$, repeating one if there are only finitely many. No choice indexed by all points was used.

Let $H_r={\bigcup }_{n\le r}\overline{B_n}$. By [L1] these are compact and closed, and their interiors cover $M$. Set $r_1=1$ and recursively take the least $r_{m+1}>r_m$ with $H_{r_m}\subseteq \mathrm{int}{H}_{r_{m+1}}$; compactness supplies such an integer. Put $K_m=H_{r_m}$ and $K_{-1}=K_0=\mathrm{\varnothing }$. Then $K_m\subseteq \mathrm{int}{K}_{m+1}$ and their interiors cover $M$. The compact annuli $C_m=K_m\setminus \mathrm{int}{K}_{m-1}$ cover $M$. The least-integer recursion spends no dependent choice.

For each $m$, take all tuples $(W,V,n)$ of smooth coordinate balls with compact closures such that $\bar{W}\subseteq V,\bar{V}\subseteq B_n\cap \mathrm{int}{K}_{m+1}\setminus K_{m-2}\mathrm{.}$ Their $W$-sets cover $C_m$, by applying [F2] twice at a point in a suitable $B_n$. By [L1] the set of finite ordered lists of these tuples covering $C_m$ is nonempty, including the empty list if $C_m=\mathrm{\varnothing }$. Use [A1] to choose one list for each $m$. The resulting pairs are indexed by a subset $I$ of ${\mathbb{N}}^2$ and cover $M$. Their $V_i$ are locally finite: a neighbourhood $\mathrm{int}{K}_t$ meets no pair from $m\ge t+2$, while the earlier finitely many annuli supply only finitely many pairs. Retain the integer $n(i)$ from each tuple.

By [L2] and [A1] choose for each $i\in I$ a smooth function $g_i:M\to [0,1]$ equal to one near ${\bar{W}}_i$ and supported in $V_i$. Their supports are locally finite, and $G={\sum }_i{g}_i$ is smooth and positive because the $W_i$ cover $M$. Thus ${\varphi }_i=g_i\mathrm{/}G$ are smooth, nonnegative, have locally finite supports contained in $V_i$, and sum to one. This is a direct normalization calculation, not an invocation of a partition theorem with unaccounted choices or indexing.

Define $\tilde{F}(y)={\sum }_{i\in I}{\varphi }_i(y)F(x_{n(i)})\mathrm{.}$ Componentwise the summands are smooth and their supports are locally finite, so [L3] and [L4] make $\tilde{F}$ smooth. At any $y$, only finitely many terms are nonzero; such indices have $y\in V_i\subseteq B_{n(i)}$ and hence $\mathrm{\parallel }F(x_{n(i)})-F(y)\mathrm{\parallel }<\epsilon (y)\mathrm{/}2$ by step 1.1. Since at least one weight is positive and their sum is one, $\mathrm{\parallel }\tilde{F}(y)-F(y)\mathrm{\parallel }\le {\sum }_i{\varphi }_i(y)\mathrm{\parallel }F(x_{n(i)})-F(y)\mathrm{\parallel }<\epsilon (y)\mathrm{/}2<\epsilon (y)\mathrm{.}$ This proves the claim, including the empty case.