LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-29 (claude-fable-5)

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.

In a Hausdorff space a sequence converges to at most one point

Statement

Let $X$ be a Hausdorff space (Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not), let $(x_{k})$ be a sequence in $X$ and let $p, q \in X$ with $x_{k} \to p$ and $x_{k} \to q$ (Convergence and cluster points of a sequence in a topological space, sequential continuity, and the sequential closure). Then $p = q$ .

So in a Hausdorff space a sequence has at most one limit, and the notation $\lim_{k} x_{k}$ that Convergence and cluster points of a sequence in a topological space, sequential continuity, and the sequential closure withholds in a general space is legitimate there.

The converse is false. Uniqueness of sequential limits does not imply the Hausdorff condition: the cocountable topology on $R$ has unique sequential limits and is not Hausdorff (FALSE: a space in which every sequence has at most one limit is Hausdorff). So this lemma is strictly weaker than the hypothesis it is proved from, and it is not a characterisation.

Facts & Assumptions

Given: A Hausdorff space $X$ , a sequence $(x_{k})$ in $X$ , and points $p, q \in X$ with $x_{k} \to p$ and $x_{k} \to q$ .

[A1]

$X$ is Hausdorff: distinct points have disjoint open neighbourhoods (Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not).

[A2]

$x_{k} \to r$ means that for every neighbourhood $N$ of $r$ there is $K \in N$ with $x_{k} \in N$ for all $k \geq K$ ; and an open set containing $r$ is a neighbourhood of $r$ (Convergence and cluster points of a sequence in a topological space, sequential continuity, and the sequential closure, Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open).

[L1]

For all $m, n \in N$ exactly one of $m < n$ , $m = n$ , $m > n$ holds, so any two natural numbers are comparable (Trichotomy of the order on $N$ ).

Proof

technique · contradiction

1.1

Suppose $p \neq q$ .

assume-contra

2.1

By [A1] there are open sets $U ∋ p$ and $V ∋ q$ with $U \cap V = \emptyset$ .

step 1.1A1

3.1

$U$ is a neighbourhood of $p$ and $V$ a neighbourhood of $q$ , so by [A2] there are $K_{1}, K_{2} \in N$ with $x_{k} \in U$ for all $k \geq K_{1}$ and $x_{k} \in V$ for all $k \geq K_{2}$ .

step 2.1A2

4.1

By [L1] the naturals $K_{1}$ and $K_{2}$ are comparable; let $K$ be whichever of them is not smaller than the other, so that $K \geq K_{1}$ and $K \geq K_{2}$ .

step 3.1L1choose

5.1

By step 3.1 and step 4.1 the term $x_{K}$ lies in $U$ and in $V$ , so $x_{K} \in U \cap V$ .

step 3.1step 4.1

6.1

Step 5.1 contradicts $U \cap V = \emptyset$ from step 2.1, so the supposition of step 1.1 fails and $p = q$ .

step 2.1step 5.1discharge-contradiction∎

Remarks

Why this is not the diagonal criterion in disguise. The criterion of this page characterises the Hausdorff condition exactly; the sequential statement above does not, and the gap is recorded by FALSE: a space in which every sequence has at most one limit is Hausdorff. A sequence sees only countably many points, and a space may separate no pair of points by open sets while still admitting no non-trivial convergent sequence at all.
No choice principle is used. The two indices $K_{1}$ and $K_{2}$ come from two named neighbourhoods, and step 4.1 compares two given naturals; nothing is selected from a family.
The statement is about limits, not about cluster points. A sequence in a Hausdorff space may well have many cluster points (Convergence and cluster points of a sequence in a topological space, sequential continuity, and the sequential closure), and nothing above bears on that.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

35 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Hausdorff space (Wikipedia) (standard reference, not scraped)
Limit of a sequence (Wikipedia) (standard reference, not scraped)
Topological Spaces lecture notes (University of Cambridge) (standard reference, not scraped)