LemmaStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-02

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 total derivative at a point is unique

Statement

If $L, M : R^{m} \to R^{n}$ both satisfy the total-differentiability remainder condition for $f$ at $a$ , then $L = M$ .

Facts & Assumptions

Given: Linear maps $L, M$ which both satisfy the definition of total derivative at $a$ .

[L1]

In the total-derivative definition, the normalized remainder tends to zero as $h$ tends to zero (The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder).

Proof

technique · direct

1.1

Subtracting the two remainder identities gives $∥ (L - M) h ∥_{2} / ∥ h ∥_{2} \to 0$ as $h \to 0$ .

2.1

For any fixed $v \in R^{m}$ and nonzero real $t$ , linearity gives $∥ (L - M) (t v) ∥_{2} / ∥ t v ∥_{2} = ∥ (L - M) v ∥_{2} / ∥ v ∥_{2}$ when $v \neq 0$ .

step 1.1algebra

3.1

Letting $t \to 0$ in step 2.1 forces $(L - M) v = 0$ for every nonzero $v$ , and it is also zero at $v = 0$ ; hence $L = M$ .

step 1.1step 2.1∎

Depends on

The total (Fréchet) derivative $Df(a)$ as the linear first-order approximation with $o(\|h\|_2)$ remainder

Used by

Dependency tree · two levels

5 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

J. Lebl, Basic Analysis I, §8.3 (standard reference, not scraped)