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

Under choice, Ornstein's second construction turns a point-finite metric open cover into a locally finite open refinement

Statement

Assume the Axiom of Choice. Every point-finite open cover of a metric space has a locally finite open refinement. Consequently every metric open cover has a locally finite open refinement.

Facts & Assumptions

Given: Choice, a metric space X, and a point-finite open cover {Cα}α∈A.

[A1]

The Axiom of Choice permits the cover to be well ordered and used to select its first eligible member (The Axiom of Choice, The well-ordering theorem).

[F1]

Metric balls are open, and every point has a positive-radius ball inside some cover member (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement).

[F2]

A locally finite open refinement is the paracompactness refinement of Refinements, locally finite families, point-finite families, and star refinements.

[L1]

Under choice every metric open cover has a point-finite open refinement (Under choice, every open cover of a metric space has a point-finite open refinement).

Proof

technique · constructive
1.1

Well order the point-finite cover. For x∈X let ρx=sup⁡{r>0:B(x,r)⊆Cα for some α}. Put mx=min⁡{1,ρx/4} when ρx<∞, and mx=1 otherwise. Then 0<mx≤1 and B(x,2mx) lies in some cover member: its radius is strictly below ρx. Assign x to the first Cα containing B(x,2mx), and let Cα′ be the union of all B(x,mx) assigned to α.

A1F1construct
2.1

The selected smaller balls cover X and each lies in its assigned Cα, so {Cα′} is an open refining cover.

step 1.1
2.2

Fix x. If Cα′ meets B(x,mx/8), choose a ball B(y,my)⊆Cα′ meeting it. We claim x∈Cα. Otherwise x∉B(y,2my), while intersection gives d(x,y)<my+mx/8; hence my<mx/8≤1/8. Thus the truncation in step 1.1 is inactive at y and ρy=4my. But B(y,5my)⊆B(x,2mx), because d(x,y)+5my<6my+mx/8<7mx/8; the right-hand ball lies in some cover member by step 1.1. This contradicts the definition of ρy. Thus x∈Cα.

step 1.1
3.1

The input cover is point-finite, so x belongs to only finitely many Cα. Step 2.2 shows that B(x,mx/8) meets only the corresponding finitely many Cα′; hence the new cover is locally finite.

step 2.2F2
4.1

Hence {Cα′} is a locally finite open refinement of the point-finite cover. For an arbitrary metric open cover, first apply [L1] and then this construction; refinement is transitive, so the result refines the original cover.

L1F2step 2.1step 3.1discharge-construct∎

Remarks

In the primary paper, part (B) is applied to the point-finite cover obtained in part (A), with that cover renamed {Cα}. Its local-finiteness test concludes that every new set meeting a fixed small ball has an index α for which x∈Cα; point-finiteness of the input is exactly what turns this conclusion into finiteness. Thus part (B) upgrades part (A) rather than restarting from the original arbitrary cover.

Depends on

Used by

Dependency tree · two levels

19 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources