Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-02
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 T1T_1 space with a compatible normal sequence of open covers is metrizable

Statement

If a T1T_1 space has a compatible normal sequence of open covers, then it is metrizable.

Facts & Assumptions

Given: A T1T_1 space XX and a compatible normal sequence (Un)nN(\mathcal U_n)_{n\in\mathbb N}.

Proof

technique · constructive
1.1

Put Vn={(x,y):ySt(x,Un)}V_n=\{(x,y):y\in\operatorname{St}(x,\mathcal U_n)\}. Each VnV_n is symmetric, contains the diagonal, and normality gives Vn+1Vn+1VnV_{n+1}\circ V_{n+1}\subseteq V_n: two successive Un+1\mathcal U_{n+1}-links lie in the star of one member, which is contained in a member of Un\mathcal U_n.

givenconstruct
2.1

Define d(x,y)d(x,y) as the smaller of 11 and the infimum of r=1k2nr\sum_{r=1}^k2^{-n_r} over finite chains x=x0,,xk=yx=x_0,\ldots,x_k=y with (xr1,xr)Vnr(x_{r-1},x_r)\in V_{n_r}, taking the infimum of an empty collection to be ++\infty. Reversing a chain gives symmetry. Concatenation gives the triangle inequality within a chain-connected component, while points in different components have distance 11; truncation at 11 preserves the triangle inequality. The diagonal chains give d(x,x)=0d(x,x)=0.

step 1.1construct
3.1

The containment in step 1.1 lets every chain of total weight below 2n12^{-n-1} be compressed, from its finest links upward, to a VnV_n-link. Hence d(x,y)<2n1d(x,y)<2^{-n-1} implies (x,y)Vn(x,y)\in V_n; conversely (x,y)Vn(x,y)\in V_n gives d(x,y)2nd(x,y)\le2^{-n}.

step 1.1step 2.1
4.1

Compatibility (i) and step 3.1 show d(x,y)>0d(x,y)>0 when xyx\ne y. Compatibility (ii), the two bounds in step 3.1, and [L1] show that the dd-balls and the original neighbourhoods contain one another at every point. Thus dd is a metric inducing the given topology.

L1step 3.1discharge-construct

Depends on

Used by

Dependency tree · next 3 levels

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