TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-01

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.

Whitney approximation for Euclidean-valued maps

Statement

Let $F : M \to R^{k}$ be continuous, where $M$ is a smooth manifold, and let $ε : M \to (0, \infty)$ be a positive continuous error function. Then there exists a smooth map $\tilde{F} : M \to R^{k}$ such that

∥ \tilde{F} (p) - F (p) ∥ < ε (p) for all p \in M .

Facts & Assumptions

Given: A continuous map $F : M \to R^{k}$ and a positive continuous error function $ε$ on $M$ .

[F1]

A positive continuous error function is a continuous map $ε : M \to (0, \infty)$ (Positive continuous error functions for strong approximation).

[L1]

Smooth partitions of unity subordinate to countable coordinate covers exist (Smooth partitions of unity exist on manifolds, Smooth partitions subordinate to a countable coordinate cover).

Proof

technique · direct

1.1

By continuity of $F$ and $ε$ , each point $p \in M$ has a coordinate neighbourhood $U_{p}$ on which $∥ F (q) - F (q^{'}) ∥ < \frac{1}{3} ε (p) and ε (q) > \frac{2}{3} ε (p)$ for all $q, q^{'} \in U_{p}$ . Choose a countable cover $(U_{i})$ of this type and points $p_{i} \in U_{i}$ .

F1givenchoose

2.1

Let $(ϕ_{i})$ be a smooth partition of unity subordinate to $(U_{i})$ , provided by [L1], and set $\tilde{F} (q) : = \sum_{i} ϕ_{i} (q) F (p_{i}) .$ This is smooth because the family is locally finite.

L1step 1.1construct

3.1

Fix $q \in M$ . Only indices with $q \in U_{i}$ contribute, so $\tilde{F} (q) - F (q) = \sum_{i} ϕ_{i} (q) (F (p_{i}) - F (q)) .$ Hence $∥ \tilde{F} (q) - F (q) ∥ \leq \sum_{i} ϕ_{i} (q) ∥ F (p_{i}) - F (q) ∥ < \sum_{i} ϕ_{i} (q) \frac{ε (q)}{2} = \frac{ε (q)}{2} < ε (q) .$ Therefore $\tilde{F}$ has the required pointwise error bound.

F1step 1.1step 2.1algebra∎

Depends on

Used by

Dependency tree · two levels

9 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Theorem 6.21 (standard reference, not scraped)