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.
Standing hypotheses on this page: a metric domain, where the target must be metric, and why the compact-open topology is built from metric compactness
This page carries several standing hypotheses, and a reader who does not know which are essential and which are bookkeeping will misread its scope. They are collected here once and then used silently.
1. "The domain is a metric space" is this page's standing convention, not a hypothesis every item needs; each Statement carries exactly what its own proof uses. Where the domain must be metric, the hypothesis is inherited rather than decorative: an item quantifying over the compact subsets of the domain reads compactness through Open cover, subcover, compact metric space, and compact subset of a metric space, and it does so because The compact-open topology on for a metric domain , with subbasis , the definition this development is built over, is stated for a metric . That restriction is a scope choice of this page and not a gap in the library. Compactness for an arbitrary topological space (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right) is developed earlier in the reading order and is available here; on a metric space the two readings of "compact subset" agree (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), so nothing below is weakened by taking the metric one. The items with a metric domain for that reason are Locally compact metric space: every point has a compact neighbourhood, In a locally compact metric space every point has arbitrarily small compact closed balls, hence a neighbourhood base of compact sets, Tube lemma: if is a compact subset of a metric space , is a topological space and is open in with , then for some open , The compact-open topology on for a metric domain , with subbasis , The topology of compact convergence on for metric and : uniform convergence on each compact subset of , For a metric domain and a metric target the compact-open topology on is the topology of compact convergence, On with and metric, uniform convergence is finer than compact convergence, which is finer than pointwise convergence, The evaluation map , , If is a locally compact metric space then the evaluation map is continuous for the compact-open topology, If is continuous then its transpose , , is continuous for the compact-open topology, with no hypothesis on beyond being metric, The exponential law: for a locally compact metric and any spaces and , transposition is a bijection between and with the compact-open topology and Dini's theorem: on a compact metric space a nondecreasing sequence of continuous real functions converging pointwise to a continuous limit converges uniformly, together with the three false statements, whose witnesses are metric spaces. Equicontinuity at a point, uniform equicontinuity, and pointwise boundedness of a family of maps between metric spaces also takes a metric domain, for a different reason: it writes a distance in the domain.
Several items on this page need no metric on the domain at all, and say so. The topology of pointwise convergence on , which is the product topology, and its restriction to and A sequence converges in the topology of pointwise convergence exactly when it converges at every point are stated for a bare set . For a nonempty set and a metric space the uniform metric is a metric on , Uniform convergence, and the topology of uniform convergence: the metric topology of the uniform metric on and on , Convergence in the uniform metric is exactly uniform convergence: one serving every point and If is complete then is complete in the uniform metric, and so is are stated for a nonempty set . A uniform limit of continuous functions is continuous, so is closed in under the uniform metric is stated for an arbitrary topological space , no distance in the domain being used anywhere in its proof. Where any of these speaks of it asks in addition only that carry a topology, continuity being meaningless otherwise.
Where a purely topological statement is nevertheless made about a metric domain, it is made through Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not: the metric topology is the topology, so the two vocabularies name one thing.
2. The target is metric exactly where a distance in it is written. The topology of pointwise convergence (The topology of pointwise convergence on , which is the product topology, and its restriction to ), the compact-open topology (The compact-open topology on for a metric domain , with subbasis ), the evaluation map (The evaluation map , ) and the exponential law (The exponential law: for a locally compact metric and any spaces and , transposition is a bijection between and with the compact-open topology) need only the open sets of the target, so there is an arbitrary topological space (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison). The uniform metric (For a nonempty set and a metric space the uniform metric is a metric on ), the topology of uniform convergence (Uniform convergence, and the topology of uniform convergence: the metric topology of the uniform metric on and on ), the topology of compact convergence (The topology of compact convergence on for metric and : uniform convergence on each compact subset of ), the comparison theorem, completeness, Dini's theorem and equicontinuity (Equicontinuity at a point, uniform equicontinuity, and pointwise boundedness of a family of maps between metric spaces) all write a distance , and there is required to be metric. The theorem that the compact-open and compact-convergence topologies agree (For a metric domain and a metric target the compact-open topology on is the topology of compact convergence) is exactly the bridge between the two regimes, and it is stated with both spaces metric because that is where both topologies are defined.
3. is nonempty wherever a supremum over is taken. The uniform metric is a real-valued supremum over . The extended real line is introduced later. This page does not use it and adopts no convention (Conventions: , unbounded sets, and the extended reals). So For a nonempty set and a metric space the uniform metric is a metric on carries the hypothesis and everything resting on it inherits it. Nothing is lost: for the set of functions has exactly one element (The product set of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space) and all questions on this page are trivial there.
4. never carries a default topology. Four topologies appear on this page, and every statement names the one it means at the point of use. Where a subset of is topologised, it carries the subspace topology of the named one.
5. Compact sets carry no separation hypothesis, and the sets are not spheres. No Hausdorff assumption is made about the target anywhere on this page (Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not); where the target is metric it is Hausdorff for free (Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not), and where it is not metric nothing here needs it. And the notation of The compact-open topology on for a metric domain , with subbasis is unrelated to the sphere of Open ball, closed ball and sphere in a metric space; no sphere is written on this page.
6. Two objects on this page are deliberately new rather than reused, and each says so where it is defined.
- For a nonempty set and a metric space the uniform metric is a metric on is not the published supremum metric. The supremum metric is a metric on the bounded real-valued functions on a nonempty set is stated for the bounded real-valued functions on a nonempty set; it cannot carry an arbitrary metric target and it cannot carry unbounded functions. The uniform metric here truncates distances at and needs no boundedness hypothesis. The companion page checks that on , where both are defined, they induce the same topology, so no second notion of convergence is created.
- Locally compact metric space: every point has a compact neighbourhood is the metric special case of Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space, the general topological notion, which the library does define and which is available at this point in the reading order. This page states the metric form and nothing else; that item's own dictionary remark records the agreement and why the agreement is immediate.
7. here is a bare set of functions with the product topology, not the vector space of The vector space of all functions with pointwise operations, and as the case . That item writes for the same underlying set when the target is a field and equips it with pointwise addition and scalar multiplication. Nothing on this page uses those operations, and the target is not assumed to carry any algebraic structure at all. Where both are in play, the algebraic structure is named.
8. General conventions of the two ambient developments apply unchanged: topologies are compared as coarser and finer, never weaker and stronger, and neighbourhoods are not required to be open. The metric conventions of Which metric axiom list this library uses, the live naming fork between semimetric and pseudometric, and why extended metrics are not treated here also apply — real-valued metrics only, no extended metrics. contains and every sequence on this page is indexed from , so every reciprocal written here is or and never .
What this page does not do. It does not prove the Ascoli-Arzelà theorem or the Stone-Weierstrass theorem, both of which belong to later pages; Equicontinuity at a point, uniform equicontinuity, and pointwise boundedness of a family of maps between metric spaces is placed here only so that the first of those pages has its vocabulary earlier in the reading order. It does not claim that the exponential law is a homeomorphism — The exponential law: for a locally compact metric and any spaces and , transposition is a bijection between and with the compact-open topology is a bijection of sets of continuous maps, and its own remark records exactly what the homeomorphism form would additionally require. And it does not claim that the compact-open topology is metrizable; the negative statement, with a witness, is on this page.
Depends on
- The topology of pointwise convergence on $Y^{X}$, which is the product topology, and its restriction to $C(X,Y)$
- Uniform convergence, and the topology of uniform convergence: the metric topology of the uniform metric on $Y^{X}$ and on $C(X,Y)$
- The topology of compact convergence on $C(X,Y)$ for metric $X$ and $Y$: uniform convergence on each compact subset of $X$
- The compact-open topology on $C(X,Y)$ for a metric domain $X$, with subbasis $S(K,V) = \{f : f[K] \subseteq V\}$
- Locally compact metric space: every point has a compact neighbourhood
- The evaluation map $e : C(X,Y) \times X \to Y$, $e(f,x) = f(x)$
- Open cover, subcover, compact metric space, and compact subset of a metric space
- Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not
- Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not
- Which metric axiom list this library uses, the live naming fork between semimetric and pseudometric, and why extended metrics are not treated here
- Conventions: $\sup \emptyset$, unbounded sets, and the extended reals
- For a nonempty set $X$ and a metric space $(Y,d)$ the uniform metric $\bar\rho(f,g) = \sup_{x} \min\{d(f(x),g(x)), 1\}$ is a metric on $Y^{X}$
- The supremum metric $d_\infty(f,g) = \sup_x |f(x) - g(x)|$ is a metric on the bounded real-valued functions on a nonempty set
- The vector space $F^{X}$ of all functions $X \to F$ with pointwise operations, and $F^{n}$ as the case $X = n = \{0, 1, \dots, n-1\}$
- The product set $\prod_{i \in I} X_i$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space
- Equicontinuity at a point, uniform equicontinuity, and pointwise boundedness of a family of maps between metric spaces
- For a metric domain and a metric target the compact-open topology on $C(X,Y)$ is the topology of compact convergence
- Metric space: $d(x,y) = 0$ iff $x = y$, symmetry, and the triangle inequality; pseudometric and ultrametric
- Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison
- Open ball, closed ball and sphere in a metric space
- The exponential law: for a locally compact metric $X$ and any spaces $Z$ and $Y$, transposition is a bijection between $C(X \times Z, Y)$ and $C(Z, C(X,Y))$ with the compact-open topology
- A uniform limit of continuous functions is continuous, so $C(X,Y)$ is closed in $Y^{X}$ under the uniform metric
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 175 results over 28 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
- Compact-open topology (Wikipedia) (standard reference, not scraped)
- Function space (Wikipedia) (standard reference, not scraped)
- J. Munkres, Topology, 2nd ed., §§21, 46 (standard reference, not scraped)