Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31
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 sets containing an entourage ball about each of their points form a topology

Statement

For a uniformity U\mathcal U on XX, call OXO\subseteq X open when every xOx\in O has an entourage EE with E[x]OE[x]\subseteq O. These open sets form a topology on XX. Its neighbourhood filter at xx has {E[x]:EU}\{E[x]:E\in\mathcal U\} as a base.

Facts & Assumptions

Given: A uniform space (X,U)(X,\mathcal U).

[A1]

Entourages contain the diagonal, are closed under finite intersection, and have symmetric square roots (Uniform space in the entourage formulation, Every uniformity has a base of symmetric entourages).

[L1]

A topology contains ,X\varnothing,X, is closed under arbitrary unions, and under binary intersections (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

Proof

technique · direct
1.1

The sets \varnothing and XX are open: the first has no points to test, and for xXx\in X every entourage ball is contained in XX.

A1
1.2

An arbitrary union of open sets is open, because a point in the union lies in one member and retains that member's entourage ball.

A1
1.3

If xOPx\in O\cap P, choose entourage balls E[x]OE[x]\subseteq O and F[x]PF[x]\subseteq P; then (EF)[x]OP(E\cap F)[x]\subseteq O\cap P, so binary intersections are open.

A1
2.1

By steps 1.1 to 1.3, the open sets form a topology by [L1].

step 1.1step 1.2step 1.3L1
3.1

Let EE be an entourage and define OE={yE[x]:F[y]E[x] for some FU}.O_E=\{y\in E[x]:F[y]\subseteq E[x]\text{ for some }F\in\mathcal U\}. This set is open. Indeed, given yOEy\in O_E, choose FF as displayed and then a symmetric GG with GGFG\circ G\subseteq F. If zG[y]z\in G[y], symmetry gives G[z](GG)[y]F[y]E[x]G[z]\subseteq(G\circ G)[y]\subseteq F[y]\subseteq E[x], so zOEz\in O_E; hence G[y]OEG[y]\subseteq O_E. Now choose a symmetric DD with DDED\circ D\subseteq E. If yD[x]y\in D[x], then D[y]E[x]D[y]\subseteq E[x], so yOEy\in O_E. Thus xD[x]OEE[x]x\in D[x]\subseteq O_E\subseteq E[x], proving that E[x]E[x] is a neighbourhood of xx.

A1step 2.1
4.1

Conversely, if NN is a neighbourhood of xx, it contains an open set OO with xOx\in O; the definition of the topology supplies an entourage EE with E[x]ONE[x]\subseteq O\subseteq N. Thus the entourage balls refine every neighbourhood, and by step 3.1 they are themselves neighbourhoods. They form a neighbourhood base by [L2].

step 2.1step 3.1L2

Depends on

Used by

Dependency tree · next 3 levels

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