TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-30

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.

Every smooth manifold admits a smooth proper exhaustion function

Statement

Every smooth manifold admits a smooth proper function $h : M \to [0, \infty)$ .

Facts & Assumptions

Given: A smooth manifold $M$ .

[L1]

The manifold admits a compact exhaustion $(K_{n})_{n \geq 1}$ (Every manifold has a compact exhaustion).

[L2]

Closed sets inside open sets admit smooth cutoffs equal to $1$ near the closed set and supported in the open set (A smooth Urysohn lemma for a closed set in an open set).

[L3]

Locally finite sums of smooth functions are smooth (A locally finite sum of smooth functions is smooth).

[A1]

Closed subsets of compact spaces are compact.

Proof

technique · direct

1.1

Let $(K_{n})$ be the exhaustion from [L1], and set $K_{0} = K_{- 1} = \emptyset$ . For each $n \geq 1$ , apply [L2] to $A_{n} : = K_{n} ∖ int (K_{n - 1})$ inside the open set $int (K_{n + 1}) ∖ K_{n - 2}$ to obtain a smooth function $ρ_{n} : M \to [0, 1]$ equal to $1$ on a neighbourhood of $A_{n}$ and supported in $int (K_{n + 1}) ∖ K_{n - 2}$ .

L1L2choose

2.1

The supports of $(ρ_{n})$ are locally finite. Indeed, if $x \in A_{m} : = K_{m} ∖ int (K_{m - 1})$ , then $supp (ρ_{n}) \subseteq int (K_{n + 1}) ∖ K_{n - 2}$ from step 1.1. If $n \leq m - 3$ , then $int (K_{n + 1}) \subseteq int (K_{m - 2}) \subseteq int (K_{m - 1})$ , so $x \notin supp (ρ_{n})$ . If $n \geq m + 3$ , then $K_{n - 2} \supseteq K_{m + 1} \supseteq K_{m}$ , so again $x \notin supp (ρ_{n})$ . Thus only $ρ_{m - 2}, ρ_{m - 1}, ρ_{m}, ρ_{m + 1}, ρ_{m + 2}$ can be nonzero at $x$ . Therefore $h : = \sum_{n \geq 1} n ρ_{n}$ is a smooth nonnegative function by [L3].

L3step 1.1algebra

3.1

If $c \geq 0$ and $N > c$ , then any point $x \notin K_{N}$ lies in some annulus $A_{n}$ with $n > N$ , so $ρ_{n} (x) = 1$ and hence $h (x) \geq n > N > c$ . Thus ${x : h (x) \leq c} \subseteq K_{N}$ , and this sublevel set is compact by [A1].

A1step 1.1step 2.1

4.1

Every closed sublevel set of $h$ is compact, so $h$ is proper.

step 3.1∎

Depends on

Used by

A proper smooth exhaustion of Euclidean space Example
A proper smooth exhaustion of the open unit ball Example

Dependency tree · two levels

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