Alphabeta MathHow 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 -valued curves on a nonempty compact interval form a complete supremum-metric space
Statement
Let be a nonempty compact interval and . Continuous -valued curves on are complete in the supremum metric
Facts & Assumptions
Given: A -Cauchy sequence in .
For a nonempty compact metric space , is complete in the supremum metric ( is complete in the supremum metric for every nonempty compact metric space ).
Any two norms on , , are equivalent (For all norms on are equivalent).
Proof
Each coordinate sequence is supremum-Cauchy, so [L1] gives a continuous coordinate limit; assembling the finitely many coordinate limits defines a continuous curve .
The maximum-coordinate errors tend uniformly to zero, and [L2] bounds the Euclidean norm by a constant multiple of the maximum norm; hence , including when is a one-point interval.
Depends on
- $C(K,\mathbb{R})$ is complete in the supremum metric for every nonempty compact metric space $K$
- For $n \ge 1$ a sequence in $\mathbb{R}^n$ converges iff each coordinate sequence converges, is Cauchy iff each coordinate sequence is Cauchy, and $\mathbb{R}^n$ is complete in every norm
- A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions
- For $n \ge 1$ all norms on $\mathbb{R}^n$ are equivalent
- Vector-valued functions $f : A \to \mathbb{R}^m$, their limits and continuity, with the dictionary to the metric notions
Used by
- A uniformly bounded equicontinuous sequence of ℝⁿ-valued curves on a nonempty compact interval has a uniformly convergent subsequence Lemma
- Picard iteration converges with geometric short-time and factorial cylinder error bounds Proposition
- Picard-Lindelöf local existence and uniqueness for first-order systems Theorem
Dependency tree · two levels
54 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
- Gerald Teschl, Ordinary Differential Equations and Dynamical Systems, Ch. 2 (standard reference, not scraped)
- Jiri Lebl, Basic Analysis I, Section 6.3 (standard reference, not scraped)