Alphabeta MathHow 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.
Total differentiability gives a local increment bound and therefore continuity
Statement
If is totally differentiable at , then some satisfy whenever and . In particular is continuous at .
Facts & Assumptions
Given: A total derivative for at .
The normalized remainder in the total-derivative definition tends to zero as tends to zero (The total (Fréchet) derivative as the linear first-order approximation with remainder).
Every Euclidean linear map has a norm bound for some (Every Euclidean linear map has a unique matrix and satisfies for some ).
Proof
By [L1], choose such that the remainder satisfies whenever .
If bounds as in [L2], the triangle inequality gives for those , and it also holds at .
Given , take ; step 2.1 is the metric continuity condition at .
Depends on
- The total (Fréchet) derivative $Df(a)$ as the linear first-order approximation with $o(\|h\|_2)$ remainder
- Every Euclidean linear map has a unique matrix and satisfies $\|Lh\|_2\le K\|h\|_2$ for some $K\ge0$
- Continuity of a map between metric spaces, at a point and globally, in the $\varepsilon$-$\delta$ form
Used by
- The map y(x²+y²)/x off the line x=0, extended by zero on that line, has every directional derivative zero at the origin but is discontinuous there Counterexample
- On a convex open set, a uniform bound ‖Df(z)v‖₂≤ M‖v‖₂ implies ‖f(y)-f(x)‖₂≤ M‖y-x‖₂ Theorem
- The chain rule for total derivatives: D(g∘ f)(a)=Dg(f(a))∘ Df(a) Theorem
- The Euclidean inverse function theorem Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 72 results over 17 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
- J. Lebl, Basic Analysis I, §8.3 (standard reference, not scraped)