Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generated
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, metric spaces have sigma-discrete open bases

Statement

Assume the Axiom of Choice. Every metric space has a σ-discrete open basis. More precisely, a well-order of the underlying set suffices; after fixing it, the construction uses no further choice.

Facts & Assumptions

[F2]

A family is discrete when each point has a neighborhood meeting at most one member; a σ-discrete basis is a union of a sequence of discrete families of open sets (Discrete families and σ-locally-finite and σ-discrete bases).

[A1]

Assume The Axiom of Choice; The well-ordering theorem supplies a well-order < of X.

Given: A metric space (X,d) and the axiom assumption A1.

Proof

1.1A1F1construct

Fix the well-order in A1. For k,n∈N and a∈X, put Ua,k=Bd(a,2−k), rn=2−n, and define Fa,k,n={z∈X:(∀y∈X∖Ua,k) d(z,y)≥rn}∖⋃b<aUb,k. The first set is closed, being the intersection over y∉Ua,k of the closed sets {z:d(z,y)≥rn}; the triangle inequality makes their complements open. Its defining condition is vacuous if Ua,k=X. The subtracted union is open, so Fa,k,n is closed, and it lies in Ua,k since a point outside that set violates the condition with y=z.

2.1F1step 1.1

For fixed k,n the nonempty cores are pairwise rn separated. Indeed, if a<b, u∈Fa,k,n and v∈Fb,k,n, then v∉Ua,k by the subtraction defining the latter core, and hence d(u,v)≥rn. For each fixed k their union over a,n is X: given x, the set of centers a with x∈Ua,k is nonempty (it contains x), so has a least member a. Openness gives some δ>0 with Bd(x,δ)⊆Ua,k. Take n with rn≤δ. Then every y∉Ua,k satisfies d(x,y)≥rn, and x lies in none of the earlier balls, so x∈Fa,k,n. These are least selections or existential instantiations, requiring no further choice.

3.1F1F2step 2.1construct

For each nonempty core define the open set Va,k,n=⋃u∈Fa,k,nBd(u,rn/3). It contains its core and is contained in Ua,k: a point outside Ua,k has distance at least rn from every core point. For fixed k,n, every ball Bd(x,rn/6) meets at most one of these sets. Otherwise two points of that ball belonging to different V sets yield corresponding core points u,v with d(u,x)<rn/2 and d(v,x)<rn/2, whence d(u,v)<rn, contradicting step 2.1. Thus each layer Vk,n={Va,k,n:Fa,k,n≠∅} is discrete, and its union over n covers X for every k.

4.1F1F2step 3.1∎

The union of all layers is a basis. If x∈O with O open, choose ε>0 with Bd(x,ε)⊆O and k with 21−k<ε. By step 3.1 some Va,k,n contains x. Both x and each z in that set lie in Ua,k, so d(x,z)<21−k<ε; therefore x∈Va,k,n⊆O. Enumerate pairs (k,n) by successive finite diagonals k+n=0,1,2,… to obtain a sequence of discrete layers. If X is empty, all layers are empty and the same basis criterion holds vacuously. This proves the claimed σ-discrete open basis, with AC used only for the initial well-order.

Depends on

Used by

Dependency tree · two levels

23 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