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 compact set inside a bounded open set admits an explicit compactly supported continuous cutoff
Statement
Let , where is compact and is bounded and open. Then there is such that , on , and .
Facts & Assumptions
Given: A compact set and a bounded open set with .
The distance-to-set map is Lipschitz (, so the distance to a fixed nonempty set is -Lipschitz).
In , compact sets are exactly closed and bounded sets, and a continuous real-valued function on a nonempty compact metric space attains a minimum (Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).
Compact support is defined by the closure of the nonzero set (The support of a function on and its compactly supported Riemann integral, The spaces and ).
Proof
If , the zero function belongs to and [L3, given, algebra] already satisfies the conclusion. So assume from now on that is nonempty.
Let . By openness of , one has for every [L1, L2, given, choose, algebra] . The function is continuous by [L1], so [L2] gives a minimum value
Define by [L1, step 1.2, construct] Because is obtained by composing the continuous function with a continuous piecewise-linear cutoff on , it is continuous and . Since on , one has on .
The nonzero set of is contained in , so [L1, L2, L3, step 2.1, algebra] The support of a function on and its compactly supported Riemann integral gives Every point of the right-hand set lies in , because means . Also is bounded, so is compact by [L2], and the closed set lies in . Hence is compact and contained in , so .
Depends on
- $|d(x,A) - d(y,A)| \le d(x,y)$, so the distance to a fixed nonempty set is $1$-Lipschitz
- Heine-Borel in $\mathbb{R}^n$: with the Euclidean metric a subset of $\mathbb{R}^n$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line
- A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value
- The support of a function on $\mathbb{R}^n$ and its compactly supported Riemann integral
- The spaces $C_c(\mathbb{R}^n)$ and $C_c^\infty(\mathbb{R}^n)$
Used by
Dependency tree · two levels
51 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
- Walter Rudin, Real and Complex Analysis, 3rd ed. (standard reference, not scraped)