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 pseudocompact subset of is bounded
Statement
Let . Every pseudocompact subset is bounded for the Euclidean metric.
Facts & Assumptions
Given: A pseudocompact subset , where has the Euclidean metric .
The Euclidean norm is continuous from to (The finite and reverse triangle inequalities for a norm; and for every norm on satisfies and is Lipschitz, hence continuous, for ).
A pseudocompact space has bounded image under every continuous real-valued map (Pseudocompact space: every continuous real-valued function has bounded image).
A subset of a metric space is bounded when it is empty or lies in some open ball (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space); a bounded set of reals has an upper bound (Lower bound, bounded below, bounded set).
Proof
The restriction , , is continuous, because the ambient norm is continuous by [L1] and has the subspace topology.
Pseudocompactness gives that is bounded. If , choose an upper bound of ; then because every norm is nonnegative.
If it is bounded. Otherwise every satisfies , so .
Thus is bounded in both cases.
Depends on
- Pseudocompact space: every continuous real-valued function has bounded image
- The finite and reverse triangle inequalities for a norm; and for $n \ge 1$ every norm $N$ on $\mathbb{R}^n$ satisfies $N(x) \le C\lVert x\rVert_1$ and is Lipschitz, hence continuous, for $d_2$
- Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space
- Lower bound, bounded below, bounded set
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 121 results over 23 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- Pseudocompact space (standard reference, not scraped)
- Heine-Borel theorem (Wikipedia) (standard reference, not scraped)