Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27
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.

Every open cover of a compact metric space has a Lebesgue number: a δ>0 such that every nonempty subset of diameter less than δ lies inside a single member of the cover

Statement

Let (X,d) be a compact metric space (Open cover, subcover, compact metric space, and compact subset of a metric space, Metric space: d(x,y)=0 iff x=y, symmetry, and the triangle inequality; pseudometric and ultrametric) and let U be an open cover of X. Then there is a real δ>0, a Lebesgue number for U, such that every nonempty A⊆X with diam⁡(A)<δ (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space) satisfies A⊆U for some U∈U.

Diameters of nonempty subsets of X are defined because a compact space is bounded (A compact subset of a metric space is closed and bounded) and a subset of a bounded set is bounded. No choice principle is used.

Facts & Assumptions

Given: A compact metric space (X,d) and an open cover U of it.

[L2]

A compact metric space is bounded, and diam⁡(A)=sup⁡{d(u,v):u,v∈A} is defined for every nonempty bounded A (A compact subset of a metric space is closed and bounded, Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space).

[L3]

For nonempty S⊆X, d(x,S)=inf⁡{d(x,y):y∈S}; an infimum is a lower bound of its set and is at least every lower bound (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space, Greatest lower bound (infimum)).

[L5]

A continuous real-valued function on a nonempty compact metric space attains a least value (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

[L6]

A nonempty finite set of reals has a maximum, one of its members (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set).

Proof

technique · direct
1.1

If X=∅ then δ:=1 serves, there being no nonempty subset of X to test; assume from now on X≠∅.

L2
2.1

Compactness gives m∈N and U0,…,Um∈U with X=U0∪⋯∪Um.

L1step 1.1
3.1

If Ui=X for some i≤m, then δ:=1 serves again, every nonempty A⊆X being contained in that Ui; assume from now on that X∖Ui≠∅ for every i≤m.

step 2.1
4.1

For α0,…,αm and β0,…,βm real one has αi≤βi+∣αi−βi∣≤max⁡jβj+max⁡j∣αj−βj∣ for every i, so max⁡iαi≤max⁡jβj+max⁡j∣αj−βj∣, and by symmetry ∣max⁡iαi−max⁡iβi∣≤max⁡i∣αi−βi∣.

L6step 3.1
5.1

Define g:X→R by g(x):=max⁡{ d(x,X∖Ui):i≤m }, a maximum of a nonempty finite set of reals; each x↦d(x,X∖Ui) changes by at most d(x,y) between x and y, so by step 4.1 ∣g(x)−g(y)∣≤d(x,y), and g is Lipschitz with constant 1, hence continuous.

L4L6step 4.1
6.1

g(x)>0 for every x∈X: such an x lies in some Ui by step 2.1, openness gives a real r>0 with B(x,r)⊆Ui, so every y∈X∖Ui has d(x,y)≥r, making r a lower bound of {d(x,y):y∈X∖Ui} and hence g(x)≥d(x,X∖Ui)≥r>0.

L3L7step 2.1step 5.1
7.1

By the extreme value theorem applied to the nonempty compact X and the continuous g, there is x∗∈X with g(x∗)≤g(x) for every x; put δ:=g(x∗), a real with δ>0 by step 6.1.

L5step 5.1step 6.1
8.1

Let A⊆X be nonempty with diam⁡(A)<δ and fix a∈A; then g(a)≥δ, so some i≤m has d(a,X∖Ui)≥δ, the maximum defining g(a) being one of its members, and the least such i may be taken.

L2L6step 7.1
9.1

Every y∈A satisfies d(a,y)≤diam⁡(A)<δ≤d(a,X∖Ui), so y∉X∖Ui, since a point of that set would make d(a,X∖Ui)≤d(a,y); hence A⊆Ui with Ui∈U, and δ is a Lebesgue number for U.

L2L3step 8.1∎

Remarks

What the lemma buys. An open cover gives, around each point, some member containing a ball about that point, with a radius depending on the point. A Lebesgue number is one radius that works everywhere at once, and that uniformity is exactly what turns pointwise continuity into uniform continuity in Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous.

Compactness is not removable. The cover of the interval (0,1) by the intervals (1/(k+2),1), k∈N, has no Lebesgue number (The cover of (0,1) by the intervals (1/(k+2),1) has no Lebesgue number, so the Lebesgue number lemma needs compactness ↗), and (0,1) is not compact.

The two degenerate cases in steps 1.1 and 3.1 are genuine. If X is empty the conclusion is vacuous, and if some member of the finite subcover is the whole space the function g of step 5.1 would call for the distance to the empty set, which this library leaves undefined (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space). Handling both separately costs two lines and avoids writing something undefined.

Depends on

Used by

Dependency tree · two levels

53 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