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
, so the distance to a fixed nonempty set is -Lipschitz
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
The support of a function on and its compactly supported Riemann integral
The spaces and