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 locally compact and -compact
Statement
For , Euclidean space is locally compact and -compact.
Facts & Assumptions
Given: with , its origin , and its Euclidean norm.
Every Euclidean closed ball of positive radius is compact (For , every Euclidean closed ball and every Euclidean sphere of positive radius is compact).
A space is locally compact when every point has a compact neighbourhood, and it is -compact when it is a countable union of compact subsets (Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space, Countably compact, Lindel"of, sequentially compact, limit point compact and -compact spaces, and relatively compact subsets).
For every real there is a natural with (Every complete ordered field is Archimedean).
Proof
For , the closed ball is compact by [L1] and contains the open ball about . Thus has a compact neighbourhood.
For each put . Every is compact by [L1].
If , [L3] gives with , so . Hence .
Step 1.1 gives local compactness and step 2.1 gives -compactness.
Depends on
- Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space
- Countably compact, Lindel\"of, sequentially compact, limit point compact and $\sigma$-compact spaces, and relatively compact subsets
- For $n\ge1$, every Euclidean closed ball and every Euclidean sphere of positive radius is compact
- Every complete ordered field is Archimedean
Used by
- Weights, their associated measures, and the spaces Lᵖ(w) Definition
- A locally integrable density functional is represented by g dlambda Example
- Følner sets in ℝⁿ Example
- Riesz measure of a log modulus records the holomorphic zeros Example
- The real affine group is amenable and nonunimodular Example
- Positive intermediate cohomology of compactified Euclidean space vanishes Lemma
- Reiter functions can be cut down to Følner sets Lemma
- Relative property (T) for SL2(R) semidirect R2 Lemma
- Topological manifolds are locally compact and locally path connected Proposition
- A normed space is locally compact if and only if it is finite-dimensional Theorem
- Lebesgue measure is a Radon measure on Rⁿ Theorem
- The distributional Riesz functional of a subharmonic function is a positive Radon measure Theorem
Dependency tree · two levels
29 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
- Sigma-compact space (standard reference, not scraped)
- Locally compact space (Wikipedia) (standard reference, not scraped)