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 chain rule, in one line from Carathéodory: if is differentiable at and is differentiable at , then is differentiable at with
Statement
Let , let with and let , so that the composite is defined. Let be a limit point of (Limit point, isolated point, adherent point, derived set, and dense subset of ) at which is differentiable (The derivative of at a point that is a limit point of , and differentiability on a set), put , and suppose is a limit point of at which is differentiable. Then is differentiable at and
Both limit-point hypotheses are needed, and neither is automatic. That is a limit point of is what makes and defined symbols; that is a limit point of is what makes one. Nothing forces the second: may be differentiable at and send to an isolated point of , and there is not defined and the formula asserts nothing.
No case analysis appears anywhere. The naive difference-quotient proof writes and then has to say what happens where , which may occur at points arbitrarily close to . Carathéodory's factorisation never divides by the inner increment, so the difficulty does not arise.
Statement references
Facts & Assumptions
Given: Sets , functions with and , a point that is a limit point of at which is differentiable, and the point , a limit point of at which is differentiable (The derivative of at a point that is a limit point of , and differentiability on a set, Limit point, isolated point, adherent point, derived set, and dense subset of ).
Carathéodory's characterisation (Carathéodory's characterisation: is differentiable at if and only if there is , continuous at , with for every , and then is unique and ), used in both directions: for , a point that is a limit point of and , the function is differentiable at if and only if there is , continuous at , with for every , and then .
Algebra of continuous functions (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function, claim 1): a product of two functions continuous at a point of their common domain is continuous there.
Composition of continuous functions (A composite of continuous functions is continuous, with no side hypothesis of the kind the composition of limits needs): if has and is continuous at , and if is continuous at , then is continuous at (Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point).
A function differentiable at a point is continuous there (A function differentiable at is continuous at ).
Proof
By [L1], applied to on at , fix , continuous at , with for every and .
By [L1], applied to on at , fix , continuous at , with for every and .
The factorisation. Let . Then , so taking in step 1.2 gives , and by step 1.1. Since , this reads for every , where is the pointwise product .
The outer factor is continuous at . By [L4] the function is continuous at ; by step 1.2 the function is continuous at ; and . So is continuous at by [L3].
The factor is continuous at , with the right value. is the product of , continuous at by step 2.2, with , continuous at by step 1.1, so is continuous at by [L2]; and .
By step 2.1 the function factors the increment of at , and by step 3.1 it is continuous at . So [L1], applied to on at the limit point , gives that is differentiable at with .
Remarks
-
Where the classical proof goes wrong, precisely. It divides by , which may vanish at points arbitrarily close to even when is differentiable at with ; the usual repair defines an auxiliary function equal to the outer quotient off the bad set and to on it, and then proves that auxiliary function continuous. That auxiliary function is , and Carathéodory's characterisation: is differentiable at if and only if there is , continuous at , with for every , and then is unique and is the observation that it exists before any repair is attempted.
-
What is composed is continuity, not differentiability. The only theorem about composites used above is A composite of continuous functions is continuous, with no side hypothesis of the kind the composition of limits needs, and it needs no side hypothesis, unlike the corresponding statement for limits. That is the whole reason the proof has no cases.
-
The formula is about the point , not about near . Both derivatives on the right are taken at single points, and the theorem says nothing about on the image of any neighbourhood of . In particular no hypothesis is placed on beyond its lying in .
Depends on
The derivative of at a point that is a limit point of , and differentiability on a set
Carathéodory's characterisation: is differentiable at if and only if there is , continuous at , with for every , and then is unique and
A composite of continuous functions is continuous, with no side hypothesis of the kind the composition of limits needs
A function differentiable at is continuous at
Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function
Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point
Limit point, isolated point, adherent point, derived set, and dense subset of