Alphabeta Math
RemarkRemark: 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.

What is fixed here and what is not: the derivative is taken at a point of the domain that is also a limit point of it, one-sided derivatives and derivatives of order above one are not introduced at this point in the reading order, and f′(c) and dfdx(c) name the same real number

This page fixes fewer conventions than a reader of a calculus text may expect, and it is worth saying which, so that a later page can rely on them and so that nothing here is read as more than it is.

Where a derivative may be taken. f′(c) is defined only when c belongs to the domain A of f and is a limit point of A (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, Limit point, isolated point, adherent point, derived set, and dense subset of R). At an isolated point of A the symbol is not defined, and the function is neither differentiable nor non-differentiable there: the question is not posed. This is inherited from The ε-δ limit lim⁡x→cf(x)=L of f:A→R at a limit point c of A, which leaves lim⁡x→c undefined at an isolated point for the reason recorded there, namely that the ε-δ condition would be satisfied vacuously by every real at once.

The domain is part of the data. "Differentiable at c" is a statement about the pair (f,A) and the point c, not about f near c in isolation. Shrinking the domain preserves differentiability and the value of the derivative whenever the smaller domain still has c as a limit point (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), but enlarging it need not, and the companion page's witness at a corner shows that it need not. Wherever a statement on this page says "differentiable at every point of (a,b)" for a function on [a,b], the domain meant is [a,b].

One-sided derivatives are not introduced at this point in the reading order. No item up to this point in the reading order defines one, and nothing below may be cited as though one had been. The ingredient is available: The left and right limits of f at c, as limits of the restrictions of f to A∩(−∞,c) and A∩(c,∞) defines the limit of f at c from the right as the limit at c of the restriction of f to A∩(c,∞) (Intervals of R: the nine order-convex forms, nondegeneracy, and length), and a right derivative would be that limit applied to the difference quotient. Nothing on this page needs it, so nothing on this page defines it. What does occur, and should not be confused with it, is the derivative at an endpoint of an interval: for f on [a,b] the symbol f′(a) is defined by 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 without any new convention, because the domain supplies points on one side of a only and the difference quotient is a function on (a,b]. So the object other texts call a one-sided derivative appears here as an ordinary derivative on a domain that happens to lie on one side.

Derivatives of order above one are not introduced at this point in the reading order either, and no item up to this point in the reading order defines one. A later page takes them up; nothing on this page anticipates it. Doing so requires more than iterating the definition: f′ is a function on the set of points at which f is differentiable, and to differentiate that function at a point one needs the point to be a limit point of that set, which is a hypothesis about f and not a formality. No statement on this page mentions f′′, and none should be read as implying anything about it.

Two notations, one object. f′(c) and dfdx(c) name the same real number. The second is a name, not a quotient: nothing in this library divides df by dx, no object called df is introduced, and the letter x in it is a name for the argument of f and not a variable that is being fixed or varied. This page writes f′(c) throughout.

Two descriptions, one notion. By Carathéodory's characterisation: f is differentiable at c if and only if there is φ:A→R, continuous at c, with f(x)−f(c)=φ(x)(x−c) for every x∈A, and then φ is unique and φ(c)=f′(c), "f is differentiable at c" may be read either as the convergence of the difference quotient or as the existence of a factorisation f(x)−f(c)=φ(x)(x−c) with φ continuous at c. The two are equivalent, and the factor is unique, so either may be taken as the meaning of the word without ambiguity. Every statement on this page is phrased in the first, and the two readings divide the proofs between them: the differentiation rules use the factorisation, namely A function differentiable at c is continuous at c, Sums, scalar multiples, products and quotients: (f+g)′(c)=f′(c)+g′(c), (αf)′(c)=αf′(c), (fg)′(c)=f′(c)g(c)+f(c)g′(c), and (f/g)′(c)=(f′(c)g(c)−f(c)g′(c))/g(c)2 when g(c)≠0, The chain rule, in one line from Carathéodory: if g is differentiable at c and f is differentiable at g(c), then f∘g is differentiable at c with (f∘g)′(c)=f′(g(c)) g′(c) and Derivative of an inverse: if f is continuous and injective on a nondegenerate interval I and differentiable at c∈I with f′(c)≠0, then the inverse g is differentiable at f(c) with g′(f(c))=1/f′(c); and if f′(c)=0 then g is not differentiable at f(c), each exhibiting a factor and reading its continuity off the algebra of continuous functions; while the rest of the page works with the difference quotient directly, among them The linear-approximation form of the derivative: f is differentiable at c with f′(c)=L if and only if the remainder r(x)=f(x)−f(c)−L(x−c) satisfies lim⁡x→cr(x)/(x−c)=0; at most one L does so, so x↦f(c)+L(x−c) is the unique affine map approximating f to first order at c, the base cases of For a natural n≥1 the function x↦xn is differentiable everywhere with derivative ι(n) x n−1; for n=0 it is the constant 1, with derivative 0; for a natural n≥1 the function x↦x−n is differentiable at every x≠0 with derivative −ι(n) x−n−1; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, and Fermat's interior extremum theorem: if f has a local extremum at a point c interior to its domain and is differentiable at c, then f′(c)=0, whose whole mechanism is the sign of the quotient near the point.

What is deliberately not claimed anywhere on this page. That f′ is continuous where it exists; that differentiability alone, with no hypothesis on f′, gives any regularity beyond the continuity of A function differentiable at c is continuous at c — a bound on f′ does give more, and that is 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; and that a vanishing derivative marks a local extremum. None of the three is addressed here, and no item on this page may be cited for any of them. What is recorded, as the two false statements of this page, is that the mean value theorem needs continuity on the closed interval and that a vanishing derivative at a point does not prevent a function from being increasing; each carries its own witness.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

46 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