LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passverified 2026-08-09 (gpt-5.6-terra-codex-subscription)

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.

A Cauchy filter with a cluster point converges to that point

Statement

A Cauchy filter on a uniform space with a cluster point $x$ converges to $x$ .

Facts & Assumptions

Given: A Cauchy filter $\mathcal F$ and one of its cluster points $x$ .

[L1]

A cluster point meets every filter member in every neighbourhood, while convergence means containment of every neighbourhood (Convergence and cluster points of a filter on a topological space).

[L2]

Cauchy filters have small members, and symmetric entourages have symmetric square roots (Cauchy filter in a uniform space, Every uniformity has a base of symmetric entourages).

[L3]

For the topology induced by a uniformity, every entourage ball $D[x]$ is a neighbourhood of $x$ (The sets containing an entourage ball about each of their points form a topology).

Proof

technique · direct

1.1

Let $E$ be an entourage and choose symmetric $D$ with $D\circ D\subseteq E$ ; choose $A\in\mathcal F$ with $A\times A\subseteq D$ .

L2choose

1.2

The ball $D[x]$ is a neighbourhood of $x$ , so it meets $A$ because $x$ is a cluster point; fix $a\in A\cap D[x]$ .

L1L3choose

2.1

For every $b\in A$ , symmetry gives $(x,a)\in D$ and smallness gives $(a,b)\in D$ , hence $(x,b)\in E$ ; so $A\subseteq E[x]$ .

step 1.1step 1.2

3.1

Every entourage ball about $x$ belongs to $\mathcal F$ by upward closure, and such balls form a neighbourhood base at $x$ , so $\mathcal F$ converges to $x$ .

step 2.1L1L3∎

Depends on

Used by

Every compact uniform space is complete Lemma

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 15 results over 6 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

J. Wodzicki, Uniform Structure (standard reference, not scraped)