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.
The topology of compact convergence on for metric and : uniform convergence on each compact subset of
Definition
Let and be metric spaces (Metric space: iff , symmetry, and the triangle inequality; pseudometric and ultrametric), each carrying its metric topology (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not), and let be the set of continuous maps (Continuity of a map of topological spaces at a point and globally). For a compact subset (Open cover, subcover, compact metric space, and compact subset of a metric space), a function and a real put
No supremum appears in this definition, deliberately: for the condition is vacuous and , whereas a supremum over the empty set does not exist in this library.
The family is a basis for a unique topology on (A family is a basis for a unique topology iff it covers the set and every point of an intersection of two members lies in a member inside that intersection; finite intersections of any subbasis form a basis, claim 1); that topology is the topology of compact convergence (also called the topology of uniform convergence on compact sets). The verification is carried out below.
Three facts, discharged here and reused on this page
(U1) A union of two compact subsets of is compact. Let be compact and let be open subsets of with . If there is nothing to prove. Otherwise each is covered by the same family, so by A subset of a metric space is open in the subspace metric exactly when it is the trace of an open set of the ambient space, and it is compact as a metric space in its own right exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it (claim 3) either , and we take the empty list for it, or there are finitely many indices whose sets cover ; concatenating the two lists gives finitely many indices whose sets cover , and that list is nonempty because is. By A subset of a metric space is open in the subspace metric exactly when it is the trace of an open set of the ambient space, and it is compact as a metric space in its own right exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it again, is compact. Nothing is selected: the indices are returned by the indexed form of compactness.
(U2) For the function is a continuous map , carrying its usual metric (The absolute value makes a metric space: is a metric, its open balls are the intervals , and it is unbounded). Indeed for ,
the first inequality by the triangle inequality for the absolute value (The triangle inequality, Absolute value in an ordered field) applied after inserting and removing , and the second by the reverse triangle inequality (The reverse triangle inequality in any metric space) applied twice, the second time after using the symmetry of . Given and a real , continuity of and of at (Continuity of a map between metric spaces, at a point and globally, in the - form, Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not) supplies reals with for and for ; then (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set) gives whenever .
(U3) For and a nonempty compact the value exists. The restriction of to the metric subspace (Isometry, isometric embedding, and the subspace metric on a subset) is continuous, the - condition at a point of being the condition for read for the points of only; is a nonempty compact metric space (Open cover, subcover, compact metric space, and compact subset of a metric space); so A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value gives a point of at which attains a greatest value.
Discharge of the basis conditions
(B1) Every lies in , so .
(B2) Let . For put if , and otherwise where , which exists by (U3) and satisfies because ; either way . Put , compact by (U1), and (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set). Then , and for : for and ,
when , and the condition is vacuous when . So contains and lies inside the intersection, which is (B2).
By A family is a basis for a unique topology iff it covers the set and every point of an intersection of two members lies in a member inside that intersection; finite intersections of any subbasis form a basis the family is therefore a basis for exactly one topology on , and the open sets of that topology are exactly the unions of members of (Basis and subbasis for a topology, and the topology generated by a family of sets).
(U4) For each the sets centred at form a neighbourhood base at (Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open). Indeed a neighbourhood of contains a basic set containing , and the (B2) computation above run with , and produces with . This is the form in which the topology is used in practice: convergence to in it is exactly uniform convergence to on each compact subset of .
Remarks
-
Why the name. says that is within of uniformly on . So a neighbourhood of in this topology controls uniformly on one compact set at a time, which is uniform convergence on each compact subset rather than on all of (Uniform convergence, and the topology of uniform convergence: the metric topology of the uniform metric on and on ).
-
Both spaces are metric here, and for different reasons. The domain must be metric because compact subset is defined only there (Open cover, subcover, compact metric space, and compact subset of a metric space); the target must be metric because a distance is written. The compact-open topology of The compact-open topology on for a metric domain , with subbasis needs only the first, and that is why it, and not this one, is the definition that survives to an arbitrary target.
-
The three auxiliary facts are stated here rather than proved three times. (U2) and (U3) together are the statement that two continuous maps into a metric space are uniformly close on a compact set by a maximum and not merely by a supremum, and that is what every interior-point argument on this page consumes.
Depends on
Open cover, subcover, compact metric space, and compact subset of a metric space
A subset of a metric space is open in the subspace metric exactly when it is the trace of an open set of the ambient space, and it is compact as a metric space in its own right exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it
Metric space: iff , symmetry, and the triangle inequality; pseudometric and ultrametric
Open ball, closed ball and sphere in a metric space
Isometry, isometric embedding, and the subspace metric on a subset
Basis and subbasis for a topology, and the topology generated by a family of sets
A family is a basis for a unique topology iff it covers the set and every point of an intersection of two members lies in a member inside that intersection; finite intersections of any subbasis form a basis
Maximum and minimum of a set
Every nonempty finite set of reals has a maximum and a minimum
Continuity of a map of topological spaces at a point and globally
Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not
Continuity of a map between metric spaces, at a point and globally, in the - form
The reverse triangle inequality in any metric space
A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value
The triangle inequality
The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement
The absolute value makes a metric space: is a metric, its open balls are the intervals , and it is unbounded
Absolute value in an ordered field
Ordered field
Complete ordered field (least-upper-bound property)
Uniform convergence, and the topology of uniform convergence: the metric topology of the uniform metric on and on
The compact-open topology on for a metric domain , with subbasis
Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open