Alphabeta Math
CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-09-09 (gpt-6-astra)
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.

A uniformly continuous real function on a subset D⊆R extends uniquely to a uniformly continuous function on the closure of D

Statement

Assume the Axiom of Choice (The Axiom of Choice).

Let D⊆R be nonempty and let f:D→R be uniformly continuous on D (Uniform continuity of f:A→R: one δ serving every pair of points of A). Write D‾ for the closure of D in R (Interior, closure, boundary and exterior of a subset of R). Then:

  1. there is a uniformly continuous g:D‾→R with g(x)=f(x) for every x∈D;
  2. g is the only continuous function D‾→R extending f (Continuity of f:A→R at a point of A and on A: the ε-δ condition, its agreement with lim⁡x→cf(x)=f(c) at a limit point, and continuity at an isolated point).

Uniform continuity is sufficient; continuity alone is not enough. The function x↦1/x is continuous on D=(0,1), whose closure is [0,1], and no continuous g:[0,1]→R extends it. Indeed continuity at 0 would give ∣g(x)−g(0)∣<1 for all sufficiently small positive x, whereas taking also x<1/(∣g(0)∣+2) gives 1/x>∣g(0)∣+2. By this corollary, x↦1/x is therefore not uniformly continuous on (0,1).

This is the metric extension theorem, read through the dictionary. The work is done by A uniformly continuous map from a dense subspace into a complete metric space extends uniquely to a uniformly continuous map on the whole space, applied to the metric space X:=D‾ with the subspace metric, its dense subset D, and the complete target (R,dR) (R and Rn for n≥1 with the Euclidean metric are complete, componentwise from the Cauchy criterion in R); Dictionary: for A⊆R with the metric d(x,y)=∣x−y∣, continuity and uniform continuity of f:A→R agree with the metric-space notions, the Lipschitz and Hölder conditions are the metric ones instantiated, and a subset of R is compact in the open-cover sense of R exactly when it is a compact metric subspace translates the hypothesis and the conclusion between the two vocabularies. The extension value is uniquely defined there. Nevertheless its proof uses countable choice, supplied here by AC, both to obtain the Cantor-intersection point and to extract an approximating sequence in the uniqueness argument.

Why later pages need exactly this. The exponential and the power functions are defined on Q first and then extended to R, and the extension step is this corollary with D the rationals of an interval; that is the use for which it is stated here rather than inside an example.

Facts & Assumptions

Given: The Axiom of Choice, a nonempty set D⊆R and a function f:D→R uniformly continuous on D; X:=D‾ with the subspace metric dX of dR(x,y)=∣x−y∣.

[L3]

Density in a metric space: A⊆X is dense in X when every point of X is adherent to A, that is when every ball of X around a point of X meets A (Interior, closure, boundary, limit point, isolated point and dense subset of a metric space).

[L5]

Extension theorem: if A is dense in a metric space X, if Y is complete and if h:A→Y is uniformly continuous, then there is a uniformly continuous g:X→Y with g∣A=h, and g is the only continuous map X→Y extending h (A uniformly continuous map from a dense subspace into a complete metric space extends uniquely to a uniformly continuous map on the whole space, Uniform continuity of a map of metric spaces: one δ serving every point, Continuity of a map between metric spaces, at a point and globally, in the ε-δ form).

Proof

technique · direct
1.1

Put X:=D‾ with the subspace metric dX, so dX(x,y)=∣x−y∣ for x,y∈X; then D⊆X, and the subspace metric that D inherits from X is again d(x,y)=∣x−y∣, the same one it inherits from R. X is nonempty, since D is and D⊆D‾.

L1L2
2.1

D is dense in the metric space X. Let x∈X and let r>0 be real. By [L2] there is t∈Nr(x)∩D, and t∈D⊆X, so t lies in the ball BX(x,r)=Nr(x)∩X of X ([L1]) and in D. Hence every ball of X around a point of X meets D, which by [L3] says D is dense in X.

step 1.1L1L2L3
2.2

Transport of the hypothesis. By [L6], applied to S:=D, the uniform continuity of f on D in the sense of Uniform continuity of f:A→R: one δ serving every pair of points of A is uniform continuity of f:(D,dD)→(R,dR) as a map of metric spaces.

step 1.1L6
3.1

By [L4] the target (R,dR) is complete, so [L5] applies with A:=D, this X, Y:=R and h:=f: there is a uniformly continuous g:X→R with g(x)=f(x) for every x∈D, and g is the only continuous map X→R extending f. The assumed AC supplies the countable choices in the supplier's Cantor-intersection construction and approximating-sequence uniqueness argument.

givenstep 2.1step 2.2L4L5
4.1

Transport of the conclusion. By [L6], applied to S:=X=D‾, uniform continuity of g as a map of metric spaces is uniform continuity of g on D‾ in the sense of Uniform continuity of f:A→R: one δ serving every pair of points of A, and continuity as a map of metric spaces is continuity on D‾ in the sense of Continuity of f:A→R at a point of A and on A: the ε-δ condition, its agreement with lim⁡x→cf(x)=f(c) at a limit point, and continuity at an isolated point. So g is uniformly continuous on D‾, extends f, and is the unique continuous extension of f to D‾: claims 1 and 2.

step 3.1L6∎

Remarks

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

69 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