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.
A function differentiable at is continuous at
Statement
Let , let and let be a limit point of (Limit point, isolated point, adherent point, derived set, and dense subset of ). If is differentiable at (The derivative of at a point that is a limit point of , and differentiability on a set) 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).
Consequently, if is differentiable on a set then is continuous at every point of .
No converse is asserted, and none holds. Continuity at does not give differentiability at , and the standard witness is worked out on the companion page.
Facts & Assumptions
Given: A set , a function and a point that is 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 ): since is differentiable at the limit point of , there is , continuous at , with for every , and .
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): sums, scalar multiples and products of functions continuous at a point of the common domain are continuous there (claim 1); and every constant function on and the identity on are continuous at every point of (claim 5).
Continuity of at is the - condition of Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point, and continuity on a set is continuity at each of its points.
Proof
Fix a function , continuous at , with for every .
The identity on and every constant function on are continuous at ; hence so is , which is the sum of the identity and the constant function with value .
The pointwise product is continuous at , being the product of two functions on continuous at .
For every one has , so is the sum of the constant function with value and the product of step 2.1.
A sum of two functions continuous at is continuous at , so is continuous at .
The point was an arbitrary point of , a limit point of , at which is differentiable; applying step 4.1 at every point of a set on which is differentiable gives continuity of at every point of .
Remarks
-
Where the work actually is. None of it is here. Carathéodory's characterisation already replaces the quotient by a product, and a product is visibly small when one factor is bounded near and the other tends to ; the algebra of continuous functions packages exactly that. A direct proof from the quotient would multiply and divide by and would have to say why that is legal, which is the same observation in a less convenient place.
-
The converse fails. is continuous at and not differentiable there, which is is continuous everywhere and not differentiable at : the difference quotient equals on the right and on the left, so the two one-sided limits differ ↗ on the companion page. So continuity is strictly weaker, and the gap is not exotic: it opens at a single corner.
-
What is not claimed. Nothing here says that a function differentiable on a set has a continuous derivative, and nothing here says that is defined anywhere except where it was assumed to be. Both are separate questions, and neither is settled on this page.
Depends on
- The derivative $f'(c) = \lim_{x \to c} \frac{f(x) - f(c)}{x - c}$ of $f : A \to \mathbb{R}$ at a point $c \in A$ that is a limit point of $A$, and differentiability on a set
- Carathéodory's characterisation: $f$ is differentiable at $c$ if and only if there is $\varphi : A \to \mathbb{R}$, continuous at $c$, with $f(x) - f(c) = \varphi(x)(x - c)$ for every $x \in A$, and then $\varphi$ is unique and $\varphi(c) = f'(c)$
- Continuity of $f : A \to \mathbb{R}$ at a point of $A$ and on $A$: the $\varepsilon$-$\delta$ condition, its agreement with $\lim_{x \to c} f(x) = f(c)$ at a limit point, and continuity at an isolated point
- 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
- Limit point, isolated point, adherent point, derived set, and dense subset of $\mathbb{R}$
Used by
- Every continuous function on an interval has a primitive; two primitives differ by a constant; and ∫ₐᵇ f = G(b)-G(a) for any primitive G Corollary
- Inside its radius a real power series may be integrated term by term on every closed subinterval Corollary
- Parity and the Pythagorean identity for sine and cosine Corollary
- A curve for which the mean value inequality is an equality, showing the constant cannot be improved Counterexample
- An invertible derivative at one point does not give a local inverse without C¹ regularity Counterexample
- f(t) = (t², t³) on [0,1]: no ξ satisfies f(1)-f(0) = f'(ξ) Counterexample
- The sign function is Riemann integrable on [-1,1] and has no primitive there Counterexample
- x ↦ |x| is continuous everywhere and not differentiable at 0: the difference quotient equals 1 on the right and -1 on the left, so the two one-sided limits differ Counterexample
- x ↦ √x on (0,1] is differentiable with unbounded derivative and is not Lipschitz there, so the boundedness hypothesis in the Lipschitz corollary cannot be dropped Counterexample
- Principal inverse sine and inverse cosine Definition
- The mean value theorem gives |√x - √y| ≤ 1/ι(2) |x - y| for x, y ≥ 1, so the square root is Lipschitz with constant 1/2 on [1,∞) Example
- FALSE: if u and v are differentiable on [a,b] then ∫ₐᵇ uv' = u(b)v(b)-u(a)v(a)-∫ₐᵇ u'v False statement
- Higher-order Rolle theorem Lemma
- Tangent is a continuous strictly increasing bijection from (-π/2,π/2) onto ℝ Lemma
- 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) and df/dx(c) name the same real number Remark
- A differentiable function on an open interval is convex if and only if its derivative is nondecreasing Theorem
- Addition formulas, identities, parity, and derivatives of the hyperbolic functions Theorem
- Continuity and derivatives of positive-base real powers Theorem
- Darboux's theorem: every derivative has the intermediate-value property Theorem
- For -1<y<1, (arcsin y)ᵖʳⁱᵐᵉ=1/√1-y² and (arccos y)ᵖʳⁱᵐᵉ=-1/√1-y² Theorem
- If u,v are differentiable on [a,b] with u',v' integrable, then ∫ₐᵇ u v' = u(b)v(b)-u(a)v(a) - ∫ₐᵇ u'v Theorem
- L'Hôpital's rule for the ∞/∞ form at finite or infinite, one-sided endpoints Theorem
- L'Hôpital's rule for the 0/0 form at finite or infinite, one-sided endpoints Theorem
- Peano's form: the normalized Taylor remainder tends to zero Theorem
- Principal arctangent: derivative, integral, power series, and the Gregory–Leibniz series Theorem
- Substitution: if φ is differentiable on [c,d] with φ' integrable and f is continuous on an interval containing φ([c,d]), then ∫_φ(c)^φ(d) f = ∫_cᵈ (f∘φ) φ' Theorem
- Sums, scalar multiples, products and quotients: (f+g)'(c) = f'(c) + g'(c), (α f)'(c) = α f'(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)² when g(c) ≠ 0 Theorem
- 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) Theorem
- The exponential is the unique solution of y'=y with y(0)=1 Theorem
- The mean value inequality: if f : [a,b] → ℝᵐ is continuous and differentiable on (a,b) with ‖ f'‖₂ ≤ M, then ‖ f(b)-f(a)‖₂ ≤ M(b-a) Theorem
- The second fundamental theorem: if G is differentiable on [a,b] with G' = f and f is integrable, then ∫ₐᵇ f = G(b)-G(a) Theorem
- Young's theorem: total differentiability of the first partials forces equality of mixed partials Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 44 results over 16 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
- Differentiable function (Wikipedia) (standard reference, not scraped)
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 5 (Thm 5.2) (standard reference, not scraped)
- J. Lebl, Basic Analysis I, §4.1 (standard reference, not scraped)
- J. Lebl, Basic Analysis I, The Derivative (standard reference, not scraped)
- T. Gantumur, Differentiation (standard reference, not scraped)