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

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)

Statement

Let A,B⊆R, let g:A→R with g[A]⊆B and let f:B→R, so that the composite f∘g:A→R is defined. Let c∈A be a limit point of A (Limit point, isolated point, adherent point, derived set, and dense subset of R) at which g is differentiable (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), put b:=g(c), and suppose b is a limit point of B at which f is differentiable. Then f∘g is differentiable at c and

(f∘g)′(c)  =  f′(g(c)) g′(c).

Both limit-point hypotheses are needed, and neither is automatic. That c is a limit point of A is what makes g′(c) and (f∘g)′(c) defined symbols; that b=g(c) is a limit point of B is what makes f′(b) one. Nothing forces the second: g may be differentiable at c and send c to an isolated point of B, and there f′(b) is not defined and the formula asserts nothing.

No case analysis appears anywhere. The naive difference-quotient proof writes f(g(x))−f(g(c))g(x)−g(c)⋅g(x)−g(c)x−c and then has to say what happens where g(x)=g(c), which may occur at points arbitrarily close to c. Carathéodory's factorisation never divides by the inner increment, so the difficulty does not arise.

Facts & Assumptions

Given: Sets A,B⊆R, functions g:A→R with g[A]⊆B and f:B→R, a point c∈A that is a limit point of A at which g is differentiable, and the point b:=g(c)∈B, a limit point of B at which f is differentiable (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).

[L1]

Carathéodory's characterisation (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)), used in both directions: for D⊆R, a point p∈D that is a limit point of D and h:D→R, the function h is differentiable at p if and only if there is η:D→R, continuous at p, with h(y)−h(p)=η(y)(y−p) for every y∈D, and then η(p)=h′(p).

[L2]
[L4]

A function differentiable at a point is continuous there (A function differentiable at c is continuous at c).

Proof

technique · direct
1.1

By [L1], applied to g on A at c, fix ψ:A→R, continuous at c, with g(x)−g(c)=ψ(x)(x−c) for every x∈A and ψ(c)=g′(c).

L1choose
1.2

By [L1], applied to f on B at b, fix φ:B→R, continuous at b, with f(y)−f(b)=φ(y)(y−b) for every y∈B and φ(b)=f′(b).

L1choose
2.1

The factorisation. Let x∈A. Then g(x)∈B, so taking y:=g(x) in step 1.2 gives f(g(x))−f(b)=φ(g(x))(g(x)−b), and g(x)−b=g(x)−g(c)=ψ(x)(x−c) by step 1.1. Since (f∘g)(c)=f(g(c))=f(b), this reads (f∘g)(x)−(f∘g)(c)=χ(x)(x−c) for every x∈A, where χ:A→R is the pointwise product χ:=(φ∘g) ψ.

step 1.1step 1.2
2.2

The outer factor is continuous at c. By [L4] the function g is continuous at c; by step 1.2 the function φ is continuous at b=g(c); and g[A]⊆B. So φ∘g is continuous at c by [L3].

step 1.2L3L4
3.1

The factor is continuous at c, with the right value. χ is the product of φ∘g, continuous at c by step 2.2, with ψ, continuous at c by step 1.1, so χ is continuous at c by [L2]; and χ(c)=φ(g(c)) ψ(c)=φ(b) ψ(c)=f′(b) g′(c).

step 1.1step 2.2L2
4.1

By step 2.1 the function χ:A→R factors the increment of f∘g at c, and by step 3.1 it is continuous at c. So [L1], applied to f∘g on A at the limit point c, gives that f∘g is differentiable at c with (f∘g)′(c)=χ(c)=f′(g(c)) g′(c).

step 2.1step 3.1L1∎

Remarks

Depends on

Used by

…and 38 more results.

Dependency tree · two levels

26 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