Alphabeta MathHow 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 manifold bump for a compact set inside an open set
Statement
Let be a smooth manifold, let be compact, and let be open with . Then there exists a smooth function that equals on an open neighbourhood of and satisfies .
Facts & Assumptions
Given: A compact set and an open set with .
Every point of admits a smooth bump supported in and equal to at that point (A chart bump at a point with prescribed support).
The standard smooth step function is smooth, takes values in , is on and on (The standard smooth step function).
An indexed ambient open cover of a compact subset has a finite subcover (A subspace is compact exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it, clause 2).
Smooth maps are continuous, and composites of smooth maps are smooth (Smooth maps are continuous, Identity maps and composites of smooth maps are smooth).
Sums and scalar multiples satisfy the coordinate derivative rules (Sums, scalar multiples, products and quotients: , , , and when ); smoothness is tested by continuous iterated coordinate derivatives in charts ( maps and multi-index derivative notation in Euclidean space).
Support means the closure in of the nonzero locus.
Proof
If , take and the empty open neighbourhood. Otherwise let be the set of all smooth whose support lies in . For each , put . These sets are open by [L3] and cover by [L1]. The family uses all eligible functions, not a simultaneous choice of one function at each point.
By [L2], there are finitely many such that contains . Define . In every chart each iterated coordinate derivative of is the sum of the corresponding continuous derivatives of the , by repeated use of [L4]. Hence and are smooth. Since all summands are nonnegative, throughout the open set .
Define . It is smooth by [F1] and [L3], takes values in , and equals one on by step 2.1.
The finite union is closed by [F2], and lies in . Off every is zero, so and . Taking the closure of the nonzero locus gives . Together with step 3.1 and the empty case in step 1.1, this proves the claim.
Depends on
- A chart bump at a point with prescribed support
- The standard smooth step function
- A subspace is compact exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it
- Smooth maps are continuous
- Identity maps and composites of smooth maps are smooth
- Sums, scalar multiples, products and quotients: $(f+g)'(c) = f'(c) + g'(c)$, $(\alpha f)'(c) = \alpha f'(c)$, $(fg)'(c) = f'(c)g(c) + f(c)g'(c)$, and $(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2}$ when $g(c) \ne 0$
- $C^k$ maps and multi-index derivative notation in Euclidean space
Used by
- Every closed subset of a manifold is the zero set of a smooth nonnegative function Corollary
- Hartogs extension by a compact-support dbar correction Corollary
- Smooth functions separate points from closed sets Corollary
- Hermitian metric and L² pairing on a compact Riemann surface Definition
- The middle-handle intersection matrix of an h-cobordism Definition
- A compactly supported cutoff of an incomplete vector field is complete Example
- Cutoff extension across a puncture in complex dimension two Example
- Dual handle presentations of a genus-g surface Example
- A cancelling disk triad has an exact C² boundary scalar Lemma
- A characteristic disk with essential boundary data produces a vanishing cycle Lemma
- A collared Whitney disk can avoid an entire compact immersed image Lemma
- A countable coordinate-bump map embeds a manifold in countable Euclidean data Lemma
- A finite characteristic circuit has C² regular port traces Lemma
- A fixed cap product glues by unique transverse flow roots Lemma
- A fixed leafwise cap gives a joint transverse product with exact collar data Lemma
- A no-transversal leaf bounds a positive accessibility region with finite inward boundary Lemma
- A small regular homotopy removes triple images and preserves transverse branch pairs Lemma
- A taut foliation of a compact connected manifold has a single closed transversal Lemma
- Adapted descending field near a compact morse band Lemma
- An isolated fixed point splits under perturbation, preserving its index Lemma
- Boundary product function on a collared cobordism Lemma
- Characteristic-disk singular images can be separated into distinct leaves relative to the boundary collar Lemma
- Compact smooth manifolds have finite CW models under countable choice Lemma
- Critical values of disjoint trajectory closures can be interchanged Lemma
- Every bordism class is realized by an embedded collapse Lemma
- Every holomorphic line bundle on a compact Riemann surface has a meromorphic section Lemma
- Finite general position for a leafwise loop Lemma
- Fixed transverse fences and their finite crossing words Lemma
- Flow reparametrization realizes a level isotopy Lemma
- For a compact Morse function, disjoint local bump perturbations can separate finitely many equal critical values without changing the Hessians Lemma
- Formal adjoints of differential operators on metric vector bundles Lemma
- Gradient-like perturbation separates adjacent critical levels Lemma
- Green's second identity on a compact bordered domain of a Riemann surface Lemma
- Handles of equal index can be attached on one level Lemma
- Immersion extension on a disk: absolute and relative parametric forms Lemma
- Local Cauchy transform with smooth parameters Lemma
- Local critical-value lowering preserves the upper sublevel Lemma
- Local morse sublevel pair is a handle pair Lemma
- Normalized gradient crosses a compact regular band in controlled time Lemma
- Positive transverse accessibility is a preorder Lemma
…and 36 more results.
Dependency tree · two levels
42 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 (standard reference, not scraped)
- Will J. Merry, Differential Geometry (standard reference, not scraped)
- Nigel Hitchin, Differentiable Manifolds (standard reference, not scraped)