Alphabeta Math
RemarkRemark: AI-adaptedProof: Not applicableSession-authored (Fable 5 assisted)judge 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)f'(c) and dfdx(c)\frac{df}{dx}(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)f'(c) is defined only when cc belongs to the domain AA of ff and is a limit point of AA (The derivative f(c)=limxcf(x)f(c)xcf'(c) = \lim_{x \to c} \frac{f(x) - f(c)}{x - c} of f:ARf : A \to \mathbb{R} at a point cAc \in A that is a limit point of AA, and differentiability on a set, Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}). At an isolated point of AA 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 ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA, which leaves limxc\lim_{x \to c} undefined at an isolated point for the reason recorded there, namely that the ε\varepsilon-δ\delta condition would be satisfied vacuously by every real at once.

The domain is part of the data. "Differentiable at cc" is a statement about the pair (f,A)(f, A) and the point cc, not about ff near cc in isolation. Shrinking the domain preserves differentiability and the value of the derivative whenever the smaller domain still has cc as a limit point (The derivative f(c)=limxcf(x)f(c)xcf'(c) = \lim_{x \to c} \frac{f(x) - f(c)}{x - c} of f:ARf : A \to \mathbb{R} at a point cAc \in A that is a limit point of AA, 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)(a,b)" for a function on [a,b][a,b], the domain meant is [a,b][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 ff at cc, as limits of the restrictions of ff to A(,c)A \cap (-\infty, c) and A(c,)A \cap (c, \infty) defines the limit of ff at cc from the right as the limit at cc of the restriction of ff to A(c,)A \cap (c, \infty) (Intervals of R\mathbb{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 ff on [a,b][a,b] the symbol f(a)f'(a) is defined by The derivative f(c)=limxcf(x)f(c)xcf'(c) = \lim_{x \to c} \frac{f(x) - f(c)}{x - c} of f:ARf : A \to \mathbb{R} at a point cAc \in A that is a limit point of AA, and differentiability on a set without any new convention, because the domain supplies points on one side of aa only and the difference quotient is a function on (a,b](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: ff' is a function on the set of points at which ff 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 ff and not a formality. No statement on this page mentions ff'', and none should be read as implying anything about it.

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

Two descriptions, one notion. By Carathéodory's characterisation: ff is differentiable at cc if and only if there is φ:AR\varphi : A \to \mathbb{R}, continuous at cc, with f(x)f(c)=φ(x)(xc)f(x) - f(c) = \varphi(x)(x - c) for every xAx \in A, and then φ\varphi is unique and φ(c)=f(c)\varphi(c) = f'(c), "ff is differentiable at cc" may be read either as the convergence of the difference quotient or as the existence of a factorisation f(x)f(c)=φ(x)(xc)f(x) - f(c) = \varphi(x)(x-c) with φ\varphi continuous at cc. 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 cc is continuous at cc, Sums, scalar multiples, products and quotients: (f+g)(c)=f(c)+g(c)(f+g)'(c) = f'(c) + g'(c), (αf)(c)=αf(c)(\alpha f)'(c) = \alpha f'(c), (fg)(c)=f(c)g(c)+f(c)g(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(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2} when g(c)0g(c) \ne 0, The chain rule, in one line from Carathéodory: if gg is differentiable at cc and ff is differentiable at g(c)g(c), then fgf \circ g is differentiable at cc with (fg)(c)=f(g(c))g(c)(f \circ g)'(c) = f'(g(c))\,g'(c) and Derivative of an inverse: if ff is continuous and injective on a nondegenerate interval II and differentiable at cIc \in I with f(c)0f'(c) \ne 0, then the inverse gg is differentiable at f(c)f(c) with g(f(c))=1/f(c)g'(f(c)) = 1/f'(c); and if f(c)=0f'(c) = 0 then gg is not differentiable at f(c)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: ff is differentiable at cc with f(c)=Lf'(c) = L if and only if the remainder r(x)=f(x)f(c)L(xc)r(x) = f(x) - f(c) - L(x-c) satisfies limxcr(x)/(xc)=0\lim_{x \to c} r(x)/(x-c) = 0; at most one LL does so, so xf(c)+L(xc)x \mapsto f(c) + L(x-c) is the unique affine map approximating ff to first order at cc, the base cases of For a natural n1n \ge 1 the function xxnx \mapsto x^{n} is differentiable everywhere with derivative ι(n)xn1\iota(n)\,x^{\,n-1}; for n=0n = 0 it is the constant 11, with derivative 00; for a natural n1n \ge 1 the function xxnx \mapsto x^{-n} is differentiable at every x0x \ne 0 with derivative ι(n)xn1-\iota(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 ff has a local extremum at a point cc interior to its domain and is differentiable at cc, then f(c)=0f'(c) = 0, whose whole mechanism is the sign of the quotient near the point.

What is deliberately not claimed anywhere on this page. That ff' is continuous where it exists; that differentiability alone, with no hypothesis on ff', gives any regularity beyond the continuity of A function differentiable at cc is continuous at cc — a bound on ff' does give more, and that is If ff is continuous on an interval II and fM|f'| \le M at every interior point, then f(x)f(y)Mxy|f(x) - f(y)| \le M|x-y| for all x,yIx,y \in I, so ff is Lipschitz with constant MM and uniformly continuous on II; 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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 110 results over 23 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources