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.

Contraction implies Lipschitz implies uniformly continuous implies continuous; every Hölder map is uniformly continuous, and a Lipschitz map on a bounded space is Hölder for every exponent

Statement

Let $(X, d_{X})$ and $(Y, d_{Y})$ be metric spaces (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric) and let $f : X \to Y$ be a function, with the three regularity conditions as in Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction. Then:

If $f$ is a contraction, it is Lipschitz.
If $f$ is Lipschitz, it is uniformly continuous (Uniform continuity of a map of metric spaces: one $δ$ serving every point).
If $f$ is uniformly continuous, it is continuous (Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form).
If $f$ is $α$ -Hölder for some rational $α$ with $0 < α \leq 1$ , it is uniformly continuous.
Suppose $X$ is nonempty and bounded, and put $R : = diam (X) + 1$ , a real with $R > 0$ (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space). If $f$ is Lipschitz with constant $L$ , then for every rational $α$ with $0 < α \leq 1$ the map $f$ is $α$ -Hölder with constant $L R^{1 - α}$ .

Claim 5 carries its boundedness hypothesis for a reason, and no unconditional "Lipschitz implies Hölder" is asserted anywhere here. On an unbounded space the implication is false; the witness and its verification are in the first remark below.

Strictness is not claimed. The five implications are asserted and nothing more; that none of them reverses is witnessed elsewhere, and those witnesses are not prerequisites of this theorem. See the second remark.

Facts & Assumptions

Given: Metric spaces $(X, d_{X})$ , $(Y, d_{Y})$ , a function $f : X \to Y$ , a real $ε > 0$ , and a rational $α$ with $0 < α \leq 1$ .

[A1]

$f$ is a contraction with constant $q$ : $f$ is Lipschitz with constant $q$ and $0 \leq q < 1$ (Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction).

[A2]

$f$ is Lipschitz with constant $L \geq 0$ : $d_{Y} (f (x), f (x^{'})) \leq L d_{X} (x, x^{'})$ for all $x, x^{'} \in X$ (Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction).

[A3]

$f$ is $α$ -Hölder with constant $C \geq 0$ : $d_{Y} (f (x), f (x^{'})) \leq C d_{X} (x, x^{'})^{α}$ for all $x, x^{'} \in X$ (Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction).

[A4]

$X$ is nonempty and bounded, so $diam (X)$ exists and $d_{X} (x, x^{'}) \leq diam (X)$ for all $x, x^{'} \in X$ (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space, Complete ordered field (least-upper-bound property)).

[L1]

Uniform continuity: one $δ > 0$ per $ε > 0$ serving every pair (Uniform continuity of a map of metric spaces: one $δ$ serving every point); continuity at a point allows $δ$ to depend on the point as well (Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form).

[L2]

Rational powers of a positive base, with $a^{1} = a$ , $a^{0} = 1$ , and the supplementary clause $0^{r} = 0$ for rational $r > 0$ (Rational powers $a^{r}$ of a positive base, Order on the rationals).

[L3]

Exponent laws for positive bases: $a^{r + s} = a^{r} a^{s}$ , $(a^{r})^{s} = a^{r s}$ , and $a^{r} > 0$ (Laws of rational exponents).

[L4]

Monotonicity in the base: for rational $r > 0$ and $0 < a < b$ one has $a^{r} < b^{r}$ (Monotonicity of $r \mapsto a^{r}$ and of $a \mapsto a^{r}$ ).

[L5]

A metric is nonnegative, and $d (x, x^{'}) = 0$ forces $x = x^{'}$ (Nonnegativity of a metric is a consequence of the other axioms, not an axiom, Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric).

[L6]

Positivity of inverses and multiplication of inequalities by positives (Inverses of positives are positive, and reciprocation reverses order, Sign rules for products and monotonicity of multiplication).

Proof

technique · direct

1.1A1A2

Claim 1 is immediate from the definitions: a contraction with constant $q$ is Lipschitz with the constant $q$ , and $q \geq 0$ .

1.2A2L1L5L6

Claim 2: assume [A2] and put $δ : = ε / (L + 1)$ , a positive real since $L + 1 > 0$ . If $d_{X} (x, x^{'}) < δ$ then, using $d_{X} (x, x^{'}) \geq 0$ , $d_{Y} (f (x), f (x^{'})) \leq L d_{X} (x, x^{'}) \leq (L + 1) d_{X} (x, x^{'}) < (L + 1) δ = ε$ ; the same $δ$ served every pair, so $f$ is uniformly continuous.

1.3L1

Claim 3: assume $f$ uniformly continuous and let $a \in X$ ; the $δ$ belonging to $ε$ satisfies $d_{X} (x, a) < δ \Rightarrow d_{Y} (f (x), f (a)) < ε$ for all $x$ , which is continuity at $a$ , and $a$ was arbitrary.

1.4A3L5

Claim 4, the case of equal points: assume [A3]; if $d_{X} (x, x^{'}) = 0$ then $x = x^{'}$ , so $d_{Y} (f (x), f (x^{'})) = 0 < ε$ whatever $δ$ is.

1.5L2L3L6choose

Claim 4, the main case: put $η : = ε / (C + 1) > 0$ and $δ : = η^{1 / α}$ , which is a positive real because $1 / α$ is a positive rational and $η > 0$ .

1.6A2A4L2L3

Claim 5: assume [A2] and [A4], put $R : = diam (X) + 1$ and $C : = L R^{1 - α}$ . Since $diam (X) \geq 0$ we have $R \geq 1 > 0$ , so $R^{1 - α}$ is defined and positive and $C \geq 0$ .

2.1step 1.5A3L2L3L4L6

Let $t : = d_{X} (x, x^{'})$ with $0 < t < δ$ . Then $t^{α} < δ^{α} = (η^{1 / α})^{α} = η^{(1 / α) α} = η^{1} = η$ , so $d_{Y} (f (x), f (x^{'})) \leq C t^{α} \leq (C + 1) t^{α} < (C + 1) η = ε$ .

2.2step 1.6A2A4L2L5

Let $x, x^{'} \in X$ and $t : = d_{X} (x, x^{'})$ ; then $0 \leq t \leq diam (X) < R$ . If $t = 0$ then $d_{Y} (f (x), f (x^{'})) \leq L \cdot 0 = 0 = C \cdot 0^{α} = C t^{α}$ , because $α > 0$ .

2.3step 1.6A2L2L3L4L6

If $t > 0$ then $t = t^{α + (1 - α)} = t^{α} t^{1 - α}$ and $t^{1 - α} \leq R^{1 - α}$ : for $α < 1$ the exponent $1 - α$ is a positive rational and $0 < t < R$ , and for $α = 1$ both sides are $1$ . Multiplying by $L t^{α} \geq 0$ gives $L t = L t^{α} t^{1 - α} \leq L R^{1 - α} t^{α} = C t^{α}$ , and hence $d_{Y} (f (x), f (x^{'})) \leq L t \leq C t^{α}$ .

3.1step 1.4step 2.1L1

Steps 1.4 and 2.1 cover every pair with $d_{X} (x, x^{'}) < δ$ , and $δ$ did not depend on the pair, so $f$ is uniformly continuous: claim 4 holds.

4.1step 1.1step 1.2step 1.3step 3.1step 2.2step 2.3∎

Steps 2.2 and 2.3 give $d_{Y} (f (x), f (x^{'})) \leq C d_{X} (x, x^{'})^{α}$ for every pair, so $f$ is $α$ -Hölder with constant $C = L R^{1 - α}$ , which is claim 5; claims 1 to 4 are steps 1.1, 1.2, 1.3 and 3.1.

Remarks

Boundedness in claim 5 cannot be dropped, and here is the witness. Take $X = Y = R$ with the usual metric and $f (x) = x$ , which is Lipschitz with constant $1$ . Suppose $f$ were $α$ -Hölder with constant $C \geq 0$ for some rational $α$ with $0 < α < 1$ , so that $∣ x - y ∣ \leq C ∣ x - y ∣^{α}$ for all reals $x, y$ . Taking $y = 0$ and $x = t$ with $t > 0$ , and writing $t = t^{α} t^{1 - α}$ (Laws of rational exponents), division by $t^{α} > 0$ gives $t^{1 - α} \leq C$ for every real $t > 0$ . At $t = 1$ this reads $1 \leq C$ , so $C > 0$ ; and then choosing a natural $n$ with $n > C^{1 / (1 - α)}$ , which exists by the Archimedean property (Every complete ordered field is Archimedean), and raising to the positive rational power $1 - α$ (Monotonicity of $r \mapsto a^{r}$ and of $a \mapsto a^{r}$ , Laws of rational exponents) gives $n^{1 - α} > (C^{1 / (1 - α)})^{1 - α} = C$ , contradicting $t^{1 - α} \leq C$ at $t = n$ . So the identity of $R$ is Lipschitz and $α$ -Hölder for no exponent $α < 1$ . A chain reading "Lipschitz implies Hölder implies uniformly continuous" is therefore false as stated, which is why claims 4 and 5 are separated here and why claim 5 carries a hypothesis.
No implication reverses, and two of the witnesses are on the companion page. The square root on $[0, \infty)$ is $1 / 2$ -Hölder and not Lipschitz ( $\sqrt{\cdot}$ on $[0, \infty)$ is uniformly continuous and exactly $1 / 2$ -Hölder, and is not Lipschitz ↗), and $x \mapsto 1 / x$ on $(0, 1)$ is continuous and not uniformly continuous ( $x \mapsto 1 / x$ is continuous on $(0, 1)$ and sends the Cauchy sequence $(1 / (k + 2))_{k \geq 0}$ to an unbounded one ↗). Both are read here as orientation only: this theorem does not depend on them and claims nothing about strictness. That a Lipschitz map need not be a contraction is visible already in the identity map, whose only Lipschitz constants are the reals $\geq 1$ .
The constant $L + 1$ and the constant $C + 1$ are there to avoid a case split. Dividing by $L$ or by $C$ would require them to be nonzero, and a Lipschitz constant or a Hölder constant is allowed to be $0$ (Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction). Enlarging the constant by $1$ is harmless, since the defining inequalities are preserved by enlarging the constant.
What claim 5 costs. The constant it produces, $L R^{1 - α}$ , grows with the diameter of $X$ , and that dependence is exactly what the unbounded counterexample above exploits: as $R \to \infty$ no single Hölder constant survives.

Contraction implies Lipschitz implies uniformly continuous implies continuous; every Hölder map is uniformly continuous, and a Lipschitz map on a bounded space is Hölder for every exponent

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources