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.
Ascoli–Arzelà in the uniform topology for nonempty compact metric domains
Statement
Assume the Axiom of Choice. Let be a nonempty compact metric space, let be a metric space, and let . The closure of in the uniform topology is compact if and only if is metric-equicontinuous and pointwise relatively compact.
Facts & Assumptions
Given: Choice, a nonempty compact metric space , a metric space , and .
For a compact Hausdorff domain, compactness of the compact-open closure is equivalent to equicontinuity and pointwise relative compactness (Ascoli–Arzelà for a compact Hausdorff domain).
On a nonempty compact metric domain, the published compact-open topology equals the uniform topology (On a nonempty compact metric domain, the compact-open topology is the uniform topology).
Topological-domain and metric equicontinuity agree on a metric domain (Topological-domain equicontinuity agrees with metric equicontinuity on a metric domain).
The general and published compact-open topologies agree on a metric domain (The general compact-open topology agrees with the published metric-domain definition).
Metric compactness agrees with compactness in the metric topology (For a metric space with its metric topology, compactness in the topological sense is compactness in the metric sense, and the two notions of compact subset coincide).
Every metric space is Hausdorff (Distinct points of a metric space have disjoint balls around them).
Proof
By [L5] and [L6], with its metric topology is compact Hausdorff, so [L1] applies to .
By [L4] and [L2], the general compact-open topology used in [L1] is the uniform topology; hence the two closures and their compactness are identical.
By [L3], the equicontinuity condition in [L1] is exactly metric equicontinuity. Pointwise relative compactness is unchanged, so [L1] becomes the claimed equivalence in both directions.
Depends on
- Ascoli–Arzelà for a compact Hausdorff domain
- On a nonempty compact metric domain, the compact-open topology is the uniform topology
- Topological-domain equicontinuity agrees with metric equicontinuity on a metric domain
- The general compact-open topology agrees with the published metric-domain definition
- For a metric space with its metric topology, compactness in the topological sense is compactness in the metric sense, and the two notions of compact subset coincide
- Distinct points of a metric space have disjoint balls around them
Used by
- Under the Axiom of Choice, a pointwise bounded equicontinuous sequence on a nonempty compact metric domain into a proper metric target has a uniformly convergent subsequence Corollary
- Under the Axiom of Choice, for a nonempty compact metric domain X and a proper metric target Y, the subsets of C(X,Y) compact in the uniform topology are exactly the families closed in that topology that are pointwise bounded and equicontinuous Corollary
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 91 results over 19 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
- The Ascoli–Arzelà Theorem, BBT (standard reference, not scraped)
- Topology, second edition, Corollary 47.4 (standard reference, not scraped)