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 and a disjoint closed set have a positive norm-distance gap
Statement
Let be a real or complex normed space. If is nonempty compact, is nonempty closed, and , then there is with No convexity, completeness, HB, or infinite choice principle is required.
Facts & Assumptions
Closed means open complement; an open set contains a positive-radius ball about each of its points (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement).
A compact subset is compact for its restricted metric, so every intrinsic open cover has a finite subcover (Open cover, subcover, compact metric space, and compact subset of a metric space).
A natural-number-indexed finite family of nonempty sets has a choice function in ZF (Every natural-number-indexed list of nonempty sets has a choice function on its family of values).
Every nonempty finite list of real numbers has a maximum and a minimum (Every nonempty finite set of reals has a maximum and a minimum).
The induced metric is over either scalar field, with the norm triangle inequality, using A norm on a real vector space, the induced metric, and the dictionary with the metric axioms over and Complex norm and complex normed space together with Realification preserves a complex norm and its metric over .
Proof
Given: A normed , nonempty compact , nonempty closed , and .
Form the set of all admissible pairs and the family . For each fixed , the open complement of contains , so some has . Then and . Thus covers without selecting radii for all simultaneously.
Each in this family is open for the restricted metric on . Indeed, if , then , and every with satisfies , so is in . Thus is an intrinsic open cover of .
Compactness gives a finite subcover with , since . For each index define . Each is nonempty by the definition of . Applying finite choice to the function supplies pairs for these finitely many indices. Repeated or cause no problem: a choice function on the set of values can be evaluated at each .
The finite list consists of positive reals, so its minimum exists and is positive, since it equals one of those reals.
For any choose an index with , possible because the finite family covers . For every , admissibility gives , whereas . Hence . This proves the uniform bound for all .
Source notes
Brezis Theorem 1.7 proof, p.7, closed-minus-compact step expanded; Teschl Corollary 5.4 proof, p.140, finite-cover step specialized to normed spaces.
Depends on
- Complex norm and complex normed space
- Open cover, subcover, compact metric space, and compact subset of a metric space
- The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement
- Every natural-number-indexed list of nonempty sets has a choice function on its family of values
- Every nonempty finite set of reals has a maximum and a minimum
- A norm on a real vector space, the induced metric, and the dictionary with the metric axioms
- Realification preserves a complex norm and its metric
Used by
- The Riemann integral functional is represented by Lebesgue measure on an interval Example
- A function with nonnegative test pairings is nonnegative a.e. Lemma
- Borel change of variables from the compact-support formula and Radon uniqueness Lemma
- Borel harmonicity and comparison of harmonic measure Theorem
- Fixed-matrix global orders and certified-action error propagation Theorem
- Locally uniform limits of harmonic functions are smooth, with all derivatives converging Theorem
- Relative geometric Hahn–Banach with the exact open, closed, and compact hypotheses Theorem
- The distributional Riesz functional of a subharmonic function is a positive Radon measure Theorem
- The strong Huygens principle in odd spatial dimensions Theorem
Dependency tree · two levels
33 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
- Haim Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, §§1.1–1.2 and §1.3 evaluation paragraph (standard reference, not scraped)
- Gerald Teschl, Topics in Real and Functional Analysis, Theorems 4.13–4.20 and §5.1 (2018 university-hosted copy) (standard reference, not scraped)