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.
Continuous functions form a commutative Banach algebra
Example
Let be a nonempty compact Hausdorff space and let carry the supremum norm . Then is a unital commutative complex Banach algebra (Unital Banach algebra), and for every its spectrum is the image of :
Facts & Assumptions
Given: A nonempty compact Hausdorff space , the algebra with pointwise operations and the supremum norm, and a function .
The image of a compact set under a continuous map is compact, and a continuous real-valued function on a nonempty compact space attains a maximum and a minimum (A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism).
A uniformly Cauchy sequence of complex-valued functions on a set converges uniformly to a function on that set (A sequence of complex-valued functions converges uniformly if and only if it is uniformly Cauchy). If the domain is a topological space and all the functions are continuous, the limit is continuous: given and , choose one function uniformly within of the limit and then use its continuity at .
A unital complex Banach algebra is an associative complex algebra with submultiplicative complete norm and unit of norm one; exactly when is invertible, and is its complement (Unital Banach algebra, Spectrum and resolvent set in a Banach algebra).
Verification
The supremum norm is finite on every : is continuous and real-valued on the nonempty compact , so it attains a maximum by [L1]; the pointwise operations make a commutative associative complex algebra with unit the constant function , and holds because for every while gives .
Completeness: a -Cauchy sequence is uniformly Cauchy, so by [L2] it converges uniformly to a continuous ; uniform convergence is convergence in the supremum norm, so is complete.
Spectral inclusion: if then : the function is continuous on the nonempty compact and attains its minimum by [L1], and would mean for some . Hence is a bounded continuous function with , and it is a two-sided inverse of ; so .
Spectral equality: conversely, if for some and were an inverse of , then evaluating the identity at would give , impossible; hence . Combined with [step 2.2], .
Depends on
- Unital Banach algebra
- Spectrum and resolvent set in a Banach algebra
- A sequence of complex-valued functions converges uniformly if and only if it is uniformly Cauchy
- A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism
Used by
- Spectrum can shrink in a larger Banach algebra Counterexample
Dependency tree · two levels
31 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
- Theo Bühler and Dietmar A. Salamon, Functional Analysis — §5.1.1 examples, printed pp. 209–214 (standard reference, not scraped)