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 manifold bump for a compact set inside an open set

Statement

Let $M$ be a smooth manifold, let $K \subseteq M$ be compact, and let $W \subseteq M$ be open with $K \subseteq W$ . Then there exists a smooth function $ρ : M \to [0, 1]$ that equals $1$ on an open neighbourhood of $K$ and satisfies $supp (ρ) \subseteq W$ .

Facts & Assumptions

Given: A compact set $K \subseteq M$ and an open set $W \subseteq M$ with $K \subseteq W$ .

[L1]

Every point of $K$ admits a smooth bump supported in $W$ and equal to $1$ at that point (A chart bump at a point with prescribed support).

[F1]

The standard smooth step function $σ$ is smooth, takes values in $[0, 1]$ , is $0$ on $(- \infty, 0]$ and $1$ on $[1, \infty)$ (The standard smooth step function).

[L2]

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).

[L3]

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

[L4]

Sums and scalar multiples satisfy the coordinate derivative rules (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ); smoothness is tested by continuous iterated coordinate derivatives in charts ( $C^{k}$ maps and multi-index derivative notation in Euclidean space).

[F2]

Support means the closure in $M$ of the nonzero locus.

Proof

technique · direct

1.1F2L1L3givenconstruct

If $K = \emptyset$ , take $ρ = 0$ and the empty open neighbourhood. Otherwise let $B$ be the set of all smooth $b : M \to [0, 1]$ whose support lies in $W$ . For each $b \in B$ , put $V_{b} = {x : b (x) > 1 / 2}$ . These sets are open by [L3] and cover $K$ by [L1]. The family uses all eligible functions, not a simultaneous choice of one function at each point.

2.1L2L4step 1.1construct

By [L2], there are finitely many $b_{1}, \dots, b_{m} \in B$ such that $V = ⋃_{i = 1}^{m} V_{b_{i}}$ contains $K$ . Define $s = \sum_{i = 1}^{m} b_{i}$ . In every chart each iterated coordinate derivative of $s$ is the sum of the corresponding continuous derivatives of the $b_{i}$ , by repeated use of [L4]. Hence $s$ and $2 s$ are smooth. Since all summands are nonnegative, $2 s > 1$ throughout the open set $V$ .

3.1F1L3step 2.1construct

Define $ρ = σ \circ (2 s)$ . It is smooth by [F1] and [L3], takes values in $[0, 1]$ , and equals one on $V$ by step 2.1.

4.1F1F2step 1.1step 2.1step 3.1∎

The finite union $F = ⋃_{i = 1}^{m} supp b_{i}$ is closed by [F2], and lies in $W$ . Off $F$ every $b_{i}$ is zero, so $s = 0$ and $ρ = σ (0) = 0$ . Taking the closure of the nonzero locus gives $supp ρ \subseteq F \subseteq W$ . Together with step 3.1 and the empty case in step 1.1, this proves the claim.

A manifold bump for a compact set inside an open set

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources