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 .
Every open cover has a finite open star-refinement (Every open cover of a compact Hausdorff space has a finite open star-refinement).
A uniform-cover structure is closed under coarsening and common refinement and has star-refinements (Uniform space in the uniform-cover formulation).
A uniform-cover structure determines an entourage uniformity with basic relations , 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
Let be the covers admitting an open refinement. It is nonempty, since is open.
Coarsening preserves membership in , and two open refinements have their intersection cover as a common open refinement.
For , take an open refinement and then its finite open star-refinement from [L1]; this is a star-refinement still witnessing membership in .
Thus satisfies [L2]. Since every open cover refines itself, every open cover belongs to .
The entourage uniformity recovered from by [L3] induces the original topology. If , choose an open refinement ; then contains an open member through , so the recovered entourage balls are neighbourhoods in the original topology. Conversely, if with open, the open cover belongs to , since Hausdorffness makes closed. By [L1] choose a finite open star-refinement , which belongs to , and choose containing . The star of lies in , rather than in , and therefore .
Hence the structure is compatible with the given topology, and every open cover is uniform.
Depends on
- Every open cover of a compact Hausdorff space has a finite open star-refinement
- Uniform space in the uniform-cover formulation
- Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right
- Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not
- 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
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
- J. Wodzicki, Uniform Structure (standard reference, not scraped)
- M. Kunzinger, General Topology (standard reference, not scraped)