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 metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement
Definition
Let be a metric space (Metric space: iff , symmetry, and the triangle inequality; pseudometric and ultrametric).
A subset is open in if for every there is a real with (Open ball, closed ball and sphere in a metric space). A subset is closed in if its complement is open.
The collection
of all open subsets is the metric topology of on . A subset of that is both open and closed is called clopen.
Two sets are open for trivial reasons. is open, because the defining condition quantifies over no points; and is open, because for every and every . Consequently and are also closed, and both are clopen.
A neighbourhood of a point is any set containing an open set that contains ; an open neighbourhood is an open set containing . In a metric space, a set is a neighbourhood of exactly when it contains some ball with . Thus is open exactly when it is a neighbourhood of each of its points, and metric balls suffice to test this condition.
The metric, not the set, determines . Two metrics on the same set may have different metric topologies, and two different metrics may have the same one; the systematic comparison is Topologically, uniformly and Lipschitz equivalent metrics on a set.
Definition references
Remarks
- What "topology" means here. is defined above as a collection of subsets of ; the abstract notion of a topological space, a collection of subsets closed under arbitrary unions and finite intersections taken as primitive data, is introduced on a later page and is not used here. What is proved here is that has exactly those closure properties (Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed), which is what licenses the word.
- Open and closed are not opposites. A set may be neither ( inside , once the usual metric is available from The absolute value makes a metric space: is a metric, its open balls are the intervals , and it is unbounded) or both ( and always, and in some spaces every subset at once, as the discrete metric on the companion page shows). "Not open" is never a synonym for "closed".
- Closedness is complementation, and nothing else, at this stage. The description of closed sets by limits of sequences, and the description of the closure as an infimum of distances, are theorems proved later on this page (The closure of a nonempty is , equals together with its limit points, and is the smallest closed superset, A point lies in the closure of iff some sequence in converges to it, and a set is closed iff it is sequentially closed), not part of the definition.