Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28
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.

If f is continuous on an interval I and ∣f′∣≤M at every interior point, then ∣f(x)−f(y)∣≤M∣x−y∣ for all x,y∈I, so f is Lipschitz with constant M and uniformly continuous on I

Statement

Let I⊆R be order-convex (Intervals of R: the nine order-convex forms, nondegeneracy, and length), let f:I→R be continuous on I (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) and differentiable at every point of I interior to I (Interior, closure, boundary and exterior of a subset of R, The derivative f′(c)=lim⁡x→cf(x)−f(c)x−c of f:A→R at a point c∈A that is a limit point of A, and differentiability on a set), and let M∈R with M≥0 satisfy

∣f′(x)∣  ≤  Mat every interior point x of I.

Then

∣f(x)−f(y)∣  ≤  M ∣x−y∣for all x,y∈I,

which is exactly the statement that f is Lipschitz with constant M on I (Lipschitz map, α-Hölder map for rational 0<α≤1, and contraction, clause 3 of 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). Consequently f is uniformly continuous on I (Uniform continuity of f:A→R: one δ serving every pair of points of A).

M≥0 is a hypothesis, not a deduction. It follows from ∣f′(x)∣≤M at any single interior point, absolute values being nonnegative, but I need have no interior point at all, and then the sign condition has to be asked for. With M≥0 assumed the conclusion is a genuine statement in every case, and at x=y it reads 0≤0.

Boundedness of f′ cannot be dropped. A function may be continuous on an interval and differentiable at every interior point with no bound on ∣f′∣, and then it need not be Lipschitz there; the companion page's square root on (0,1] is such a function.

Facts & Assumptions

Given: An order-convex I⊆R, a function f:I→R continuous on I and differentiable at every interior point of I, and a real M≥0 with ∣f′(x)∣≤M at every interior point x of I.

[L1]

Mean value theorem (The mean value theorem, as the case g(x)=x of Cauchy's: for f continuous on [a,b] with a<b and differentiable on (a,b) there is c∈(a,b) with f(b)−f(a)=f′(c)(b−a)): for u<v and h:[u,v]→R continuous on [u,v] and differentiable at every point of (u,v), there is c∈(u,v) with h(v)−h(u)=h′(c)(v−u).

[L2]

Order-convexity (Intervals of R: the nine order-convex forms, nondegeneracy, and length): u,v∈I with u≤v gives [u,v]⊆I; and for u<v in I every x∈(u,v) is interior to I, since Nε(x)⊆(u,v)⊆I for ε:=min⁡{x−u, v−x}>0 (The ε-neighbourhood and the punctured ε-neighbourhood of a point of R, Interior, closure, boundary and exterior of a subset of R).

[L3]

Restriction of the domain (The derivative f′(c)=lim⁡x→cf(x)−f(c)x−c of f:A→R at a point c∈A that is a limit point of A, and differentiability on a set): if B⊆A, if p∈B is a limit point of B and if h:A→R is differentiable at p, then h∣B is differentiable at p with the same derivative; every point of an order-convex set with at least two elements is a limit point of it (Limit point, isolated point, adherent point, derived set, and dense subset of R).

[L5]

Absolute value (Basic properties of the absolute value): ∣u∣≥0; ∣u∣=0 exactly when u=0; ∣uw∣=∣u∣ ∣w∣; and ∣−u∣=∣u∣, so ∣x−y∣=∣y−x∣.

[L6]

Dictionary (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, clause 3): for a real L≥0, "f:A→R is Lipschitz with constant L" means exactly that ∣f(x)−f(x′)∣≤L ∣x−x′∣ for all x,x′∈A, this being the metric condition of Lipschitz map, α-Hölder map for rational 0<α≤1, and contraction instantiated at A⊆R with d(x,y)=∣x−y∣.

[L8]

Multiplying non-strict inequalities of nonnegatives (Multiplying inequalities of positives): 0≤s≤t and 0≤w≤z imply sw≤tz.

Proof

technique · direct
1.1

Let x,y∈I. If x=y then ∣f(x)−f(y)∣=∣0∣=0 and M∣x−y∣=M⋅0=0, so the asserted inequality holds. Assume therefore x≠y, and put u:=min⁡{x,y} and v:=max⁡{x,y}, so that u,v∈I, u<v, and ∣x−y∣=v−u=∣v−u∣ by [L5].

givenL5
2.1

By [L2] the segment [u,v] lies in I and is nondegenerate; the restriction f∣[u,v] is continuous on [u,v] by [L4]; and each x′∈(u,v) is interior to I by [L2], hence a point at which f is differentiable with ∣f′(x′)∣≤M, while x′ is a limit point of [u,v] by [L3], so f∣[u,v] is differentiable at x′ with the same derivative.

step 1.1L2L3L4
3.1

By step 2.1 the function f∣[u,v] satisfies the hypotheses of [L1], so fix c∈(u,v) with f(v)−f(u)=f′(c) (v−u).

step 2.1L1choose
4.1

Taking absolute values in step 3.1 and using ∣uw∣=∣u∣∣w∣ gives ∣f(v)−f(u)∣=∣f′(c)∣ ∣v−u∣. The point c lies in (u,v), hence is interior to I by step 2.1, so 0≤∣f′(c)∣≤M; and 0≤∣v−u∣≤∣v−u∣. So [L8] gives ∣f′(c)∣ ∣v−u∣≤M ∣v−u∣, whence ∣f(v)−f(u)∣≤M ∣v−u∣. Since {u,v}={x,y} and ∣f(v)−f(u)∣=∣f(x)−f(y)∣ by [L5], and ∣v−u∣=∣x−y∣ by step 1.1, this is ∣f(x)−f(y)∣≤M ∣x−y∣.

step 2.1step 3.1L5L8
5.1

The pair x,y∈I was arbitrary and the case x=y was settled in step 1.1, so ∣f(x)−f(y)∣≤M∣x−y∣ for all x,y∈I. By [L6] that is the statement that f is Lipschitz with constant M on I, and by [L7] such an f is uniformly continuous on I.

step 1.1step 4.1L6L7∎

Remarks

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