Alphabeta Math
LemmaStatement: 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.

Every uniformizable space is regular

Statement

Every uniformizable topological space is regular, in ZF.

Facts & Assumptions

Given: A topology induced by a uniformity, a closed CC, and xCx\notin C.

[L1]

Entourage balls form neighbourhood bases and entourages have iterated square roots (The sets containing an entourage ball about each of their points form a topology, Uniform space in the entourage formulation).

[L3]

Symmetric entourages have square roots, and a point is outside the closure of a set when it has a neighbourhood disjoint from that set (Every uniformity has a base of symmetric entourages, Interior, closure, boundary, exterior, derived set and isolated point in a topological space).

Proof

technique · direct
1.1

Since XCX\setminus C is an open neighbourhood of xx, choose an entourage EE with E[x]XCE[x]\subseteq X\setminus C, then choose a symmetric DD with D2ED^{\circ2}\subseteq E.

L1L3choose
1.2

Let OO be the union of all open subsets of D[x]D[x] containing xx. Then OO is open and xOD[x]x\in O\subseteq D[x] because D[x]D[x] is a neighbourhood.

L1construct
2.1

One has OE[x]\overline O\subseteq E[x]. Indeed, if yE[x]y\notin E[x], then the neighbourhood D[y]D[y] is disjoint from OO: a point zD[y]OD[y]D[x]z\in D[y]\cap O\subseteq D[y]\cap D[x] would give (x,y)D2E(x,y)\in D^{\circ2}\subseteq E by symmetry. Hence yOy\notin\overline O by [L3].

step 1.1step 1.2L1L3
3.1

Since E[x]C=E[x]\cap C=\varnothing, step 2.1 gives CXOC\subseteq X\setminus\overline O. The two open sets OO and XOX\setminus\overline O are disjoint neighbourhoods of xx and CC, so the space is regular by [L2].

step 1.1step 2.1L2

Depends on

Used by

Dependency tree · next 3 levels

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