TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-09-09 (Codex)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Relative Whitney approximation for Euclidean-valued maps

Statement

Assume countable choice ${A C}_{ω}$ . Let $F : M \to R^{k}$ be continuous, let $A \subseteq M$ be closed, and suppose $F$ is smooth on an open neighbourhood of $A$ . For every positive continuous error function $ε$ on $M$ , there exists a smooth map $\tilde{F} : M \to R^{k}$ such that:

$\tilde{F} = F$ on some open neighbourhood of $A$ , and
$∥ \tilde{F} (p) - F (p) ∥ < ε (p)$ for all $p \in M$ .

No compactness of $A$ or of a neighbourhood of $A$ is assumed.

Facts & Assumptions

Given: Countable choice, a continuous map $F : M \to R^{k}$ , a closed set $A \subseteq M$ , an open neighbourhood $U$ of $A$ on which $F$ is smooth, and a positive continuous error function $ε$ .

[A1]

Countable choice is assumed for the two existence results below; their countable coordinate, annular-cover and bump selections are explicitly licensed (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[L1]

Under [A1], Euclidean Whitney approximation gives a smooth $Q : M \to R^{k}$ with $∥ Q - F ∥ < ε$ pointwise (Whitney approximation for Euclidean-valued maps).

[L2]

Under [A1], there is a smooth $χ : M \to [0, 1]$ equal to one on an open neighbourhood of $A$ and with $supp (χ) \subseteq U$ (A smooth Urysohn lemma for a closed set in an open set).

[L3]

A continuous map that is smooth on an open cover is smooth globally (Smoothness is local on the source).

[L4]

Finite sums and products of smooth scalar functions, and hence componentwise scalar-vector products, are smooth by iterated coordinate derivative rules (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , $C^{k}$ maps and multi-index derivative notation in Euclidean space).

Proof

technique · direct

1.1A1L1L2givenconstruct

Use [L1] to obtain $Q$ and [L2] to obtain $χ$ . Let $W$ be an open neighbourhood of $A$ on which $χ = 1$ . Define on all of $M$ $\tilde{F} = χ F + (1 - χ) Q .$ This is a continuous Euclidean-valued map, since $F, Q, χ$ are continuous and the formula uses finite scalar sums and products. These are two applications of the explicitly assumed countable-choice existence results, not a compact-neighbourhood selection.

2.1L2L3L4step 1.1

On $U$ , the formula for $\tilde{F}$ is smooth by [L4], since $F ∣_{U}$ , $Q ∣_{U}$ and $χ ∣_{U}$ are smooth. On the open set $M ∖ supp (χ)$ it equals $Q$ , hence is smooth. These two open sets cover $M$ because $supp (χ) \subseteq U$ . Therefore [L3] proves that $\tilde{F}$ is globally smooth; no differentiability of $F$ outside $U$ is used.

3.1L1L2step 1.1step 2.1algebra∎

On $W$ , $χ = 1$ and hence $\tilde{F} = F$ . At every $p \in M$ , $∥ \tilde{F} (p) - F (p) ∥ = (1 - χ (p)) ∥ Q (p) - F (p) ∥ \leq ∥ Q (p) - F (p) ∥ < ε (p) .$ The weak inequality before the final strict inequality includes the case $χ (p) = 1$ . Thus both claims hold. The same construction includes empty $A$ (its neighbourhood can be empty), empty $M$ , and noncompact closed $A$ .

Depends on

Dependency tree · 2 levels

Sources

John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Theorem 6.21, pp.136-137