Alphabeta Math
TheoremStatement: AI-adaptedProof: 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.

The covers admitting an open refinement form a compatible uniform-cover structure on a nonempty compact Hausdorff space; in particular every open cover is uniform

Statement

For a nonempty compact Hausdorff space, the covers that admit an open refinement form a compatible uniform-cover structure. In particular every open cover is uniform.

Facts & Assumptions

Given: A nonempty compact Hausdorff space XX.

[L1]

Every open cover has a finite open star-refinement (Every open cover of a compact Hausdorff space has a finite open star-refinement).

[L2]

A uniform-cover structure is closed under coarsening and common refinement and has star-refinements (Uniform space in the uniform-cover formulation).

[L3]

A uniform-cover structure determines an entourage uniformity with basic relations EV=VVV×VE_{\mathcal V}=\bigcup_{V\in\mathcal V}V\times V, and entourage balls form neighbourhood bases for the induced topology (On a nonempty set, entourage uniformities and uniform-cover structures determine one another, The sets containing an entourage ball about each of their points form a topology).

Proof

technique · direct
1.1

Let C\mathfrak C be the covers admitting an open refinement. It is nonempty, since {X}\{X\} is open.

construct
2.1

Coarsening preserves membership in C\mathfrak C, and two open refinements have their intersection cover as a common open refinement.

step 1.1
2.2

For VC\mathcal V\in\mathfrak C, take an open refinement and then its finite open star-refinement from [L1]; this is a star-refinement still witnessing membership in C\mathfrak C.

L1step 1.1
3.1

Thus C\mathfrak C satisfies [L2]. Since every open cover refines itself, every open cover belongs to C\mathfrak C.

step 2.1step 2.2L2
4.1

The entourage uniformity recovered from C\mathfrak C by [L3] induces the original topology. If VC\mathcal V\in\mathfrak C, choose an open refinement W\mathcal W; then EW[x]=St(x,W)E_{\mathcal W}[x]=\operatorname{St}(x,\mathcal W) contains an open member through xx, so the recovered entourage balls are neighbourhoods in the original topology. Conversely, if xOx\in O with OO open, the open cover {O,X{x}}\{O,X\setminus\{x\}\} belongs to C\mathfrak C, since Hausdorffness makes {x}\{x\} closed. By [L1] choose a finite open star-refinement W\mathcal W, which belongs to C\mathfrak C, and choose W0WW_0\in\mathcal W containing xx. The star of W0W_0 lies in OO, rather than in X{x}X\setminus\{x\}, and therefore EW[x]=St(x,W)St(W0,W)OE_{\mathcal W}[x]=\operatorname{St}(x,\mathcal W)\subseteq\operatorname{St}(W_0,\mathcal W)\subseteq O.

step 3.1L1L3
5.1

Hence the structure is compatible with the given topology, and every open cover is uniform.

step 3.1step 4.1

Depends on

Used by

Dependency tree · next 3 levels

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