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 manifold-valued maps
Statement
Assume countable choice . Let be continuous, let be closed, and suppose is smooth on an open neighbourhood of . Then there exist a smooth map and an open neighbourhood of such that on and is homotopic to by a homotopy fixed on , hence relative to . No compactness of or its neighbourhood is assumed.
Facts & Assumptions
Given: Countable choice, a continuous , a closed , and an open on which is smooth.
Countable choice is The Axiom of Countable Choice (). Both existence constructions cited below explicitly assume it.
The proof of Whitney approximation for manifold-valued maps, steps 1.1 through 6.1, supplies under [A1] an embedding , a smooth inverse for , an open , and a smooth retraction . Specifically it uses the repaired arbitrary finite-dimensional embedding, defines bounded eligible normal-addition radii before taking their supremum, proves the continuous radius and its endpoint injectivity, and glues the local inverses on . These auxiliary data are fully proved there, independent of the final approximation step, without a smooth-radius minorant or a general ambient tube theorem.
Under [A1], for every positive continuous , a continuous Euclidean-valued map smooth near a closed has a smooth approximation equal to it on some open neighbourhood of and with pointwise error strictly less than (Relative Whitney approximation for Euclidean-valued maps). This statement permits arbitrary noncompact closed .
Distance to a fixed nonempty set is finite and -Lipschitz (, so the distance to a fixed nonempty set is -Lipschitz).
Composites of smooth maps are smooth, and smooth maps are continuous (Identity maps and composites of smooth maps are smooth, Smooth maps are continuous).
A homotopy relative to is a jointly continuous map on with the prescribed endpoints and constant in the second variable on (Homotopies of continuous maps, homotopies relative to a subspace, and path homotopies relative to the endpoints).
Proof
If , take the empty maps and . Otherwise is nonempty because exists. Use [L1] to obtain , and put . The map is continuous on and smooth on by [L4]. All the embedding and retraction data are fixed before applying any approximation result.
If is empty, put . Otherwise put This is finite and continuous by [L3] and continuity of the minimum operation. It is positive: at each , openness supplies a ball of some positive radius contained in , so every point of is at least that far away. This is a pointwise argument, not a simultaneous selection of radii. Moreover for every : when is nonempty, a point of in that ball would have distance to less than , contradicting the infimum lower bound. When is empty the inclusion is automatic.
Apply [L2] to , and . Obtain a smooth with everywhere and on an open neighbourhood of . Set , still an open neighbourhood of . Step 2.1 gives . Since is open, is smooth in the same coordinate charts. Thus is smooth by [L4]. For , and fixes , giving . No relatively compact neighbourhood of has been selected.
Define for . At every such pair, including because . Therefore the whole segment lies in the single ball from step 2.1 and hence in . Each coordinate of is a sum of products of continuous functions pulled back from the two factors, so is jointly continuous. The formula is consequently jointly continuous, using [L4] and the subspace topology on . Its endpoints are and , since fixes .
On the equality makes for every , and hence throughout . Thus [F1] gives a homotopy fixed on the open neighbourhood , in particular relative to . The proof also covers by permitting its open neighbourhood to be empty, and the empty-source case was settled in step 1.1. This proves every claimed conclusion.
Depends on
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- Whitney approximation for manifold-valued maps
- Relative Whitney approximation for Euclidean-valued maps
- $|d(x,A) - d(y,A)| \le d(x,y)$, so the distance to a fixed nonempty set is $1$-Lipschitz
- Identity maps and composites of smooth maps are smooth
- Smooth maps are continuous
- Homotopies of continuous maps, homotopies relative to a subspace, and path homotopies relative to the endpoints
Used by
- A continuous map from a closed subset extends smoothly exactly when it has a continuous extension and is smooth near the subset Corollary
- A homology cobordism need not be an h-cobordism Counterexample
- A compressible leaf yields a vanishing cycle Lemma
- A normal summand of rank at least two realizes every framing-loop obstruction Lemma
- A null-homotopic closed transversal yields a vanishing cycle Lemma
- Algebraic open inclusions surject on fundamental groups Lemma
- Belt-sphere complements in low handle levels preserve the fundamental group Lemma
- Compatible smooth simplex faces have a neighbourhood extension Lemma
- Frame fields with prescribed boundary conditions along a clean Whitney disk Lemma
- General position makes a Whitney disk embedded and interior-disjoint in the stable range Lemma
- General-position isotopies of links Lemma
- Geometric Gauss-Manin Hodge variations and integral lattices Lemma
- Kernel classes are represented by embedded spheres below the middle dimension Lemma
- Real Stiefel spaces with complement rank at least two are simply connected Lemma
- Relative smoothing of a continuous simplex along its faces Lemma
- Smoothing continuous families of formal immersions Lemma
- The components of the frame bundle of a connected manifold Lemma
- The fundamental-group label controls contractibility of the Whitney circle Lemma
- The Whitney framing extends over a clean disk in the stable range Lemma
- Transverse based homotopies give normal cobordisms Lemma
- Zero- and one-handles are eliminated in a simply connected h-cobordism Lemma
- Surgery on a normal map preserves its normal bordism class Proposition
- Whitney disjunction removes algebraically cancelling double points Proposition
- Continuously homotopic smooth maps are smoothly homotopic Theorem
- The mod 2 intersection number is homotopy invariant Theorem
- The universal Pontryagin-Thom correspondence for unoriented and oriented bordism Theorem
- The Whitney trick in the codimension-two borderline case Theorem
Dependency tree · two levels
46 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., Theorems 6.21 and 6.26, pp.136-137 and 141 (standard reference, not scraped)