Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-09-10 (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 manifold-valued maps

Statement

Assume countable choice ACω. Let F:M→N be continuous, let A⊆M be closed, and suppose F is smooth on an open neighbourhood of A. Then there exist a smooth map F~:M→N and an open neighbourhood W of A such that F~=F on W and F is homotopic to F~ by a homotopy fixed on W, hence relative to A. No compactness of A or its neighbourhood is assumed.

Facts & Assumptions

Given: Countable choice, a continuous F:M→N, a closed A⊆M, and an open V⊇A on which F is smooth.

[A1]

Countable choice is The Axiom of Countable Choice (ACω). Both existence constructions cited below explicitly assume it.

[L1]

The proof of Whitney approximation for manifold-valued maps, steps 1.1 through 6.1, supplies under [A1] an embedding j:N→Rk, a smooth inverse j−1:S→N for S=j(N), an open U⊇S, and a smooth retraction R:U→S. 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 {∥v∥<r(p)/2}. These auxiliary data are fully proved there, independent of the final approximation step, without a smooth-radius minorant or a general ambient tube theorem.

[L2]

Under [A1], for every positive continuous ε:M→(0,∞), a continuous Euclidean-valued map smooth near a closed A has a smooth approximation equal to it on some open neighbourhood of A and with pointwise error strictly less than ε (Relative Whitney approximation for Euclidean-valued maps). This statement permits arbitrary noncompact closed A.

[L4]

Composites of smooth maps are smooth, and smooth maps are continuous (Identity maps and composites of smooth maps are smooth, Smooth maps are continuous).

[F1]

A homotopy relative to A is a jointly continuous map on M×[0,1] with the prescribed endpoints and constant in the second variable on A (Homotopies of continuous maps, homotopies relative to a subspace, and path homotopies relative to the endpoints).

Proof

technique · direct
1.1A1L1L4givenchoose

If M=∅, take the empty maps and W=∅. Otherwise N is nonempty because F exists. Use [L1] to obtain j,S,U,R, and put f=j∘F. The map f is continuous on M and smooth on V by [L4]. All the embedding and retraction data are fixed before applying any approximation result.

2.1L3step 1.1constructalgebra

If C=Rk∖U is empty, put ε≡1. Otherwise put ε(x)=min⁡{1,12d(f(x),C)}. This is finite and continuous by [L3] and continuity of the minimum operation. It is positive: at each f(x)∈U, openness supplies a ball of some positive radius contained in U, so every point of C is at least that far away. This is a pointwise argument, not a simultaneous selection of radii. Moreover B(f(x),ε(x))⊆U for every x: when C is nonempty, a point of C in that ball would have distance to f(x) less than ε(x)≤d(f(x),C)/2, contradicting the infimum lower bound. When C is empty the inclusion is automatic.

3.1A1L1L2L4step 1.1step 2.1choose

Apply [L2] to f, A and ε. Obtain a smooth H:M→Rk with ∥H(x)−f(x)∥<ε(x) everywhere and H=f on an open neighbourhood W0 of A. Set W=W0∩V, still an open neighbourhood of A. Step 2.1 gives H(M)⊆U. Since U is open, H:M→U is smooth in the same coordinate charts. Thus F~=j−1∘R∘H is smooth by [L4]. For x∈W, H(x)=j(F(x)) and R fixes S, giving F~(x)=F(x). No relatively compact neighbourhood of A has been selected.

4.1L1L4step 1.1step 2.1step 3.1constructalgebra

Define z(x,t)=(1−t)f(x)+tH(x) for (x,t)∈M×[0,1]. At every such pair, ∥z(x,t)−f(x)∥=t∥H(x)−f(x)∥<ε(x), including t=0 because ε(x)>0. Therefore the whole segment lies in the single ball from step 2.1 and hence in U. Each coordinate of z is a sum of products of continuous functions pulled back from the two factors, so z is jointly continuous. The formula H(x,t)=j−1(R(z(x,t))) is consequently jointly continuous, using [L4] and the subspace topology on U. Its endpoints are F and F~, since R fixes S.

5.1F1step 1.1step 3.1step 4.1algebra∎

On W the equality H=f makes z(x,t)=f(x) for every t, and hence H(x,t)=F(x) throughout W×[0,1]. Thus [F1] gives a homotopy fixed on the open neighbourhood W, in particular relative to A. The proof also covers A=∅ 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

Used by

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