Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedverified 2026-09-26 (gpt-6-sol)
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.

A finite coordinate-bump map embeds a compact manifold in some Euclidean space

Statement

Let Mn be a compact smooth manifold. Then there are finitely many coordinate charts (Ui,xi), open sets Vi⊆Ui covering M, and smooth bump functions ϕi:M→[0,1] supported in Ui and equal to 1 on Vi such that F:=(ϕ1,ϕ1x11,…,ϕ1x1n,…,ϕm,ϕmxm1,…,ϕmxmn):M→Rm(n+1) is a smooth embedding.

Facts & Assumptions

Given: A compact smooth n-manifold M.

[L1]

For every point of a smooth manifold, the construction in A chart bump at a point with prescribed support, Proof 2.1–5.1, gives a chart (U,x), an open neighbourhood V⋐U of the point, and a smooth bump supported in U and equal to 1 on V.

[L2]

An injective immersion from a compact manifold is an embedding (An injective immersion from a compact manifold is an embedding).

Proof

technique · direct
1.1L1given

Let T be the family of all triples ((U,x),V,ϕ) where (U,x) is a coordinate chart, V⋐U is open, and ϕ:M→[0,1] is a smooth bump supported in U and equal to 1 on V. By [L1], the family of their open sets V covers M. Compactness gives finitely many such sets Vi covering M; retain a witnessing chart (Ui,xi) and bump ϕi for each of these finitely many sets. This uses only finite choices after the subcover is found.

2.1step 1.1construct

Define the coordinate-bump blocks Bi(q):=(ϕi(q),ϕi(q)xi1(q),…,ϕi(q)xin(q))∈Rn+1, and let F:=(B1,…,Bm). The map is smooth because each block is smooth on Ui and vanishes off Ui.

2.2step 1.1algebra

To prove immersion, fix p∈M and choose i with p∈Vi. Because ϕi is identically 1 on the open set Vi, its differential vanishes there. Thus on Vi the last n coordinates of Bi are just the chart coordinates xi1,…,xin, whose differentials form an isomorphism TpM→Rn. Hence dFp is injective.

3.1step 1.1step 2.1algebra

To prove injectivity, suppose F(p)=F(q). Choose i with p∈Vi. Then ϕi(p)=1, hence ϕi(q)=1 as well because the first coordinates of Bi(p) and Bi(q) agree. Therefore q∈Ui, and the equalities ϕi(p)xia(p)=ϕi(q)xia(q) give xia(p)=xia(q) for every a. Since xi is injective on Ui, one gets p=q.

4.1L2step 3.1step 2.2∎

Steps 3.1 and 2.2 show that F is an injective immersion. By [L2], F is a smooth embedding.

Depends on

Used by

Dependency tree · two levels

19 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