LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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 $\mathbb{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 \mathbb{N}$ with $x_k \in N$ for all $k \ge 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 \mathbb{N}$ exactly one of $m < n$ , $m = n$ , $m > n$ holds, so any two natural numbers are comparable (Trichotomy of the order on $\mathbb{N}$ ).

Proof

technique · contradiction

1.1

Suppose $p \ne q$ .

assume-contra

2.1

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

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 \mathbb{N}$ with $x_k \in U$ for all $k \ge K_1$ and $x_k \in V$ for all $k \ge 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 \ge K_1$ and $K \ge 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 = \varnothing$ 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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 89 results over 25 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click 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)