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.
Convergence and cluster points of a sequence in a topological space, sequential continuity, and the sequential closure
Definition
Let be a topological space (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison), with neighbourhoods as in Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open.
A sequence in is a function , written with . As everywhere in this library contains (The natural numbers (von Neumann)) and a sequence is indexed from (Sequences of reals: bounded, eventually, frequently, tails, subsequences); an index range copied from a text that starts at must be shifted before it is used here. The range of is . Following Sequences of reals: bounded, eventually, frequently, tails, subsequences, a property of indices holds eventually if it holds for all for some , and frequently if for every it holds for some ; that vocabulary is used here for sequences in an arbitrary set.
Let be a sequence in and let .
- converges to , written , if for every neighbourhood of one has eventually. The point is then called a limit of .
- is a cluster point of if for every neighbourhood of one has frequently.
- For , the sequential closure of is
- A function into a topological space is sequentially continuous at if in implies in , and sequentially continuous if it is sequentially continuous at every point of (Continuity of a map of topological spaces at a point and globally for the ordinary notion).
The notation is not available at this generality, and the reason is not fastidiousness. In a general topological space a sequence may converge to more than one point, so there is no function taking a convergent sequence to "its" limit, and a symbol would not denote. In the indiscrete topology on a set with at least two points the only neighbourhood of any point is , so every sequence converges to every point; in the cofinite topology on an infinite set every injective sequence converges to every point. Both witnesses are on the companion page. Accordingly this library writes " is a limit of " and " converges to ", never "the limit" and never , for a sequence in a space that has not been given a hypothesis restoring uniqueness.
Where the notation becomes legitimate again. Uniqueness of limits is what licenses the symbol, exactly as it does for sequences of reals (A sequence has at most one limit) and in a metric space (A sequence in a metric space has at most one limit): in a metric space a sequence has at most one limit and is unambiguous. Every metrizable space therefore admits the notation, and so does every space in which distinct points have disjoint neighbourhoods; where this page uses a metrizable space, and only there, the usual notation is used without further comment. The general reading of "" above never presupposes it.
Convergence agrees with the metric notion on a metric topology. For a metric space the balls around are a neighbourhood base at (The balls , , form a countable neighbourhood base at , so every metric space is first countable), so "eventually in every neighbourhood of " and "eventually in every ball around " are the same condition, and the latter is Convergence of a sequence in a metric space: iff in . The identification is carried out where metrizable spaces are defined, later on this page.
Remarks
-
Every limit is a cluster point, and not conversely. "Eventually" implies "frequently", so a point to which converges is a cluster point of it. A sequence in a two-point discrete space that takes each of the two values frequently has both points as cluster points and converges to neither, since each singleton is a neighbourhood of its point and is missed frequently.
-
Constant sequences. If for every , then , since every neighbourhood of contains . More generally an eventually constant sequence with eventual value converges to . This is the only convergence available in a discrete space, where is a neighbourhood of and forces eventually.
-
Sequential continuity is a strictly weaker condition than continuity in general, and the two agree under a countability hypothesis proved later on this page. That is the whole reason sequences are treated here as a separate notion rather than as the definition of continuity, and it is why nets and filters exist as a subject.
Depends on
Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison
Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open
Sequences of reals: bounded, eventually, frequently, tails, subsequences
The natural numbers (von Neumann)
Continuity of a map of topological spaces at a point and globally
A sequence has at most one limit
A sequence in a metric space has at most one limit
The balls , , form a countable neighbourhood base at , so every metric space is first countable
Convergence of a sequence in a metric space: iff in