Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicablejudge 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.

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

Definition

Throughout, R is the complete ordered field (Complete ordered field (least-upper-bound property)), neighbourhoods are those of The ε-neighbourhood and the punctured ε-neighbourhood of a point of R and limit points those of Limit point, isolated point, adherent point, derived set, and dense subset of R.

Let A⊆R, let f:A→R and let c∈A be a limit point of A. The difference quotient of f at c is the function

qf,c:A∖{c}→R,qf,c(x):=f(x)−f(c)x−c.

The division is legitimate at every point of the domain, since x≠c gives x−c≠0.

The point c is a limit point of A∖{c}, not merely of A. For every real ε>0 the punctured neighbourhood Nε∗(c) omits c, so

Nε∗(c)∩A  =  Nε∗(c)∩(A∖{c}),

and the left-hand side is nonempty because c is a limit point of A. So qf,c is a function on a set having c as a limit point, and lim⁡x→cqf,c(x) is a notion that The ε-δ limit lim⁡x→cf(x)=L of f:A→R at a limit point c of A defines.

f is differentiable at c when that limit exists, and then the derivative of f at c is

f′(c)  :=  lim⁡x→cqf,c(x)  =  lim⁡x→cf(x)−f(c)x−c.

Two obligations are carried by that notation, and both are discharged here.

  1. Uniqueness. Writing f′(c) treats the right-hand side as a name for a single real number. That is legitimate: c is a limit point of the domain A∖{c} of qf,c, so at most one real can satisfy the ε-δ condition, by At a limit point of the domain a function has at most one limit applied to qf,c. Two reals both meeting the condition are therefore equal, and the symbol denotes.
  2. Meaningfulness. The hypothesis that c is a limit point of A is not decoration. At an isolated point of A the punctured condition 0<∣x−c∣<δ is met by no point of the domain at all, so the ε-δ formula is satisfied vacuously by every real at once; this is why The ε-δ limit lim⁡x→cf(x)=L of f:A→R at a limit point c of A leaves the limit undefined there, and it is why this library defines f′(c) only at a limit point of A. At an isolated point of its domain a function is neither differentiable nor non-differentiable here: the question is not posed.

The limit sees only A∖{c}, so how the difference quotient is extended to c is irrelevant. Let Q:A→R agree with qf,c at every point of A∖{c}, and let L∈R. Then lim⁡x→cQ(x)=L if and only if lim⁡x→cqf,c(x)=L. Both conditions read: for every real ε>0 there is a real δ>0 such that every point x of the relevant domain with 0<∣x−c∣<δ satisfies ∣⋅−L∣<ε (The ε-δ limit lim⁡x→cf(x)=L of f:A→R at a limit point c of A). The clause 0<∣x−c∣ removes x=c from both quantifiers, so in both cases the points quantified over are exactly the x∈A∖{c} with 0<∣x−c∣<δ, at which Q and qf,c take the same value. The two conditions are the same condition.

Differentiability on a set. For S⊆A, f is differentiable on S when it is differentiable at every c∈S; implicit in that phrase is that every point of S is a limit point of A. f is differentiable when it is differentiable on the whole of A.

Restriction of the domain. Let B⊆A, let c∈B and suppose c is a limit point of B. If f is differentiable at c, then so is the restriction f∣B:B→R, and

(f∣B)′(c)  =  f′(c).

Indeed B∖{c}⊆A∖{c}; the displayed identity of punctured neighbourhoods above, applied to B, shows that c is a limit point of B∖{c}; the difference quotient qf∣B,c is the restriction of qf,c to B∖{c}, since f∣B(c)=f(c); and claim 2 of The limit at c depends only on the restriction of f to a punctured neighbourhood of c, and passes to any subset of the domain having c as a limit point carries the limit to that restriction.

Every point of a nondegenerate interval is a limit point of it. Let J⊆R be order-convex (Intervals of R: the nine order-convex forms, nondegeneracy, and length) with at least two elements and let p∈J. Choose q∈J with q≠p, and let a real ε>0 be given. If p<q, put y:=p+12min⁡{ε, q−p}; then p<y, and y−p≤12(q−p)<q−p, so p<y<q and order-convexity gives y∈J, while 0<∣y−p∣<ε. If q<p, the point y:=p−12min⁡{ε, p−q} serves in the same way. So Nε∗(p)∩J≠∅ for every real ε>0, that is, p is a limit point of J (Limit point, isolated point, adherent point, derived set, and dense subset of R).

Consequently, for f defined on a nondegenerate interval I, the symbol f′(c) is meaningful at every c∈I, endpoints included. At an endpoint the difference quotient is taken over the points of I lying on the one side that is available, so what other texts call a one-sided derivative is, here, simply the derivative of f on I.

Remarks

Depends on

Used by

…and 55 more results.

Dependency tree · two levels

21 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