Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-09-08 (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.

A chart bump at a point with prescribed support

Statement

Let M be a smooth manifold, let p∈M, and let W⊆M be open with p∈W. Then there exists a smooth function ρ:M→[0,1] such that ρ(p)=1 and supp⁡(ρ)⊆W.

Facts & Assumptions

Given: A smooth manifold M, a point p∈M, and an open neighbourhood W of p.

[F1]

Smooth charts are diffeomorphisms onto open subsets of Euclidean space (Chart maps are diffeomorphisms onto Euclidean open sets).

[L1]

Compact sets inside Euclidean open sets admit smooth bumps with prescribed support (A Euclidean bump for a compact set inside an open set).

[L2]

Smooth maps that agree on overlaps paste to a smooth global map, and composites of smooth maps are smooth (Smooth maps paste over an open cover, Identity maps and composites of smooth maps are smooth).

[F2]

For a real-valued function on M, its support means the closure in M of its nonzero locus.

Proof

technique · direct
1.1F1F2L4givenconstruct

If M has dimension zero, each singleton is open by the chart condition and is closed since M is Hausdorff. Define ρ(p)=1 and ρ=0 elsewhere. This is locally constant, hence smooth in charts, and its support is {p}⊆W. Henceforth assume the dimension n is positive.

2.1F1L1L3step 1.1choose

Choose a smooth chart (U,φ) with p∈U and put a=φ(p). Since φ(W∩U) is open, choose ε>0 with Bε(a)⊆φ(W∩U), and put R=ε/2, r=R/2. Then B‾R(a)⊆φ(W∩U). By [L3], B‾r(a) is compact. Apply [L1] inside BR(a) to obtain a smooth ρ~:Rn→[0,1] equal to one on B‾r(a) with support in BR(a).

3.1F1L3L4step 2.1construct

The closed ball B‾R(a) is compact by [L3]. Its image K=φ−1(B‾R(a)) under the continuous inverse chart, viewed as a map into M, is compact by [L4]. Thus K is closed in M and K⊆W∩U.

4.1L2step 2.1step 3.1construct

On the open cover U∪(M∖K), use ρ=ρ~∘φ on U and ρ=0 on M∖K. The functions agree on U∖K, since its coordinate image misses B‾R(a) and hence the support of ρ~. Composition and pasting in [L2] give a smooth global real-valued function whose values lie in [0,1].

5.1F2step 1.1step 2.1step 3.1step 4.1∎

The function equals one at p by step 2.1. Its nonzero locus is contained in the closed set K by step 4.1, so [F2] gives supp⁡ρ⊆K⊆W. This proves the positive-dimensional case, and step 1.1 proves the zero-dimensional case.

Depends on

Used by

Dependency tree · two levels

69 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