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.
Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not
Definition
A topological space (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison) is metrizable if there is a metric on (Metric space: iff , symmetry, and the triangle inequality; pseudometric and ultrametric) whose metric topology is , that is (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). Such a is said to induce or metrise .
The definition presupposes that is a topology in the sense of Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison, and it is. By 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 both and are open in , which is (T1), and by Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed the family is closed under arbitrary unions, which is (T2), and under intersections of members, which contains (T3). So every metric space is a topological space, and the metric-space development of this library is a special case of the present one.
The standard local notions in the two developments agree. Let be a metric on and give the topology .
-
Neighbourhoods and balls. 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 and Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open use the same convention: a neighbourhood of contains an open set containing . Open neighbourhoods are cofinal in this neighbourhood filter. The balls , (Open ball, closed ball and sphere in a metric space), are open (Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed) and form a neighbourhood base at : any neighbourhood contains an open , hence a ball around by 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 balls of radius alone already suffice (The balls , , form a countable neighbourhood base at , so every metric space is first countable).
-
Interior, closure, boundary. Interior, closure, boundary, limit point, isolated point and dense subset of a metric space defines them by the same conditions with balls in place of neighbourhoods, and the previous bullet makes the two conditions equivalent; the metric closure is the smallest closed superset (The closure of a nonempty is , equals together with its limit points, and is the smallest closed superset), which is the definition used here (Interior, closure, boundary, exterior, derived set and isolated point in a topological space). So the two closures, the two interiors and the two boundaries are the same three operations.
-
Convergence. in the sense of Convergence and cluster points of a sequence in a topological space, sequential continuity, and the sequential closure is "eventually in every neighbourhood of ", and by the first bullet this is "eventually in every ball around ", which is Convergence of a sequence in a metric space: iff in .
-
Continuity. - continuity at (Continuity of a map between metric spaces, at a point and globally, in the - form) says that every ball around has a ball around mapped into it, which by the first bullet is continuity at in the sense of Continuity of a map of topological spaces at a point and globally.
-
Subspaces. For the subspace topology of Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace is exactly the metric topology of the subspace metric (Isometry, isometric embedding, and the subspace metric on a subset), so the two uses of the phrase subspace topology in this library name one thing. Indeed : a trace is -open, since each of its points has and hence ; and a -open is the trace of , which is -open, satisfies , and involves no choice principle, the union being taken over a set of pairs rather than over a selection.
Consequently the metric-space notions of interior, closure, boundary, density, convergence, continuity and subspace agree with the topological notions here, and statements about them transfer once a metric is named. The metric and topological neighbourhood collections also agree.
Metrizability is a topological property; the metric is not part of it. If is a homeomorphism (Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological) and metrises , then is a metric on — the three axioms transfer along the bijection — and , so carries a basis of to a basis of and . Hence is metrizable. The metric itself, however, is not determined by the topology: two metrics on one set may induce the same topology without agreeing, which is exactly topological equivalence (Topologically, uniformly and Lipschitz equivalent metrics on a set), and properties of a metric that are not properties of its topology, boundedness among them, are therefore not properties of a metrizable space.
Two things every metrizable space has. It is Hausdorff: distinct points have disjoint open neighbourhoods, by Distinct points of a metric space have disjoint balls around them applied to any metric inducing the topology. And it is first countable (First countable space: a countable neighbourhood base at every point), by The balls , , form a countable neighbourhood base at , so every metric space is first countable. Either failure is therefore an obstruction to metrizability, and this page uses the first of them to exhibit a topology induced by no metric.
Sequential limits in a metrizable space are unique, so the notation is available there. In a metric space a sequence has at most one limit (A sequence in a metric space has at most one limit), and by the agreement of convergence above that uniqueness is a statement about the topology alone; so within a metrizable space, and only there, this page writes in the ordinary way. In a general space the symbol is unavailable (Convergence and cluster points of a sequence in a topological space, sequential continuity, and the sequential closure).
The usual topology of . The absolute value makes a metric space under , its open balls are the bounded open intervals, and the resulting metric topology is what claim 3 of The absolute value makes a metric space: is a metric, its open balls are the intervals , and it is unbounded names the usual topology of . That is the topology meant by the phrase throughout these two pages, and carrying it is metrizable by definition. Every statement about it on these two pages is proved from the metric and the bridge above, and no example re-derives any of it.
Remarks
-
The usual topology of is not a second notion alongside the order-native development built earlier in this library. Which results on this page use the order of and therefore have no general-topological analogue records that the two collections of open subsets of — the one defined from balls and the one defined from order-neighbourhoods — are literally the same collection, and hence that interior, closure, boundary, limit point, density and sequential convergence agree on the two sides. That identification is quoted here for orientation only; the order-topology example on the companion page is where the order-native description is used.
-
A metrizable space comes with many metrics and no canonical one. The statement " is metrizable" asserts existence, and every argument that uses a metric must name one first. Where two metrics are compared, the vocabulary is that of Topologically, uniformly and Lipschitz equivalent metrics on a set: Lipschitz, uniform and topological equivalence, of which only the last is visible to the topology.
-
Metrization theorems are not proved here. Necessary conditions are easy — Hausdorff, first countable — and sufficient ones require separation and countability axioms that this page does not develop. Nothing below asserts that a space is metrizable except by exhibiting a metric.
-
Not every topology is metrizable, and the cheapest witness is the indiscrete topology on a two-point set, which is not Hausdorff. That is recorded on this page as a false statement and witnessed on the companion page.
Depends on
Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison
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
Metric space: iff , symmetry, and the triangle inequality; pseudometric and ultrametric
Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed
Topologically, uniformly and Lipschitz equivalent metrics on a set
Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace
Isometry, isometric embedding, and the subspace metric on a subset
Open ball, closed ball and sphere in a metric space
Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open
Interior, closure, boundary, exterior, derived set and isolated point in a topological space
Continuity of a map of topological spaces at a point and globally
Convergence and cluster points of a sequence in a topological space, sequential continuity, and the sequential closure
Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological
First countable space: a countable neighbourhood base at every point
The balls , , form a countable neighbourhood base at , so every metric space is first countable
Distinct points of a metric space have disjoint balls around them
Convergence of a sequence in a metric space: iff in
Continuity of a map between metric spaces, at a point and globally, in the - form
The closure of a nonempty is , equals together with its limit points, and is the smallest closed superset
Interior, closure, boundary, limit point, isolated point and dense subset of a metric space
A sequence in a metric space has at most one limit
The absolute value makes a metric space: is a metric, its open balls are the intervals , and it is unbounded