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.
is dense in for
Statement
Assume the Axiom of Countable Choice.
Let . Then is dense in .
Facts & Assumptions
Given: The Axiom of Countable Choice, , , and .
is dense in ( is dense in for ).
Mollifier families are approximate identities, and convolution with a mollifier is smooth (A unit-mass smooth bump generates an approximate identity, Convolution with a mollifier is smooth, and derivatives pass under the integral sign).
Approximate identities converge in , and for bounded continuous functions the convergence is uniform on compacta (Every approximate identity converges to the identity in for , approximate identities converge uniformly on compacta for bounded continuous functions).
The support of a convolution lies in the closure of the support sumset (The support of a convolution lies in the closure of the support sumset).
Proof
By [L1], choose with . [L1, L2, given, choose] Let be a mollifier family as in [L2].
By [L3], choose so small that [L2, L3, L4, step 1.1, choose] . The function is smooth by [L2]. Because has compact support and has compact support, [L4] gives compact support for , so .
Therefore [step 1.1, step 2.1, algebra] Hence is dense in .
Depends on
is dense in for
A unit-mass smooth bump generates an approximate identity
Convolution with a mollifier is smooth, and derivatives pass under the integral sign
Every approximate identity converges to the identity in for
approximate identities converge uniformly on compacta for bounded continuous functions
The support of a convolution lies in the closure of the support sumset