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.
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
- A uniform limit of smooth functions need not be differentiable anywhere Corollary
- Every continuous f with f(xy)=f(x)+f(y) is f(x)=c log x for a unique c, including c=0 Corollary
- Every continuous function on [0,1] is uniformly approximated by everywhere-differentiable functions whose derivative vanishes at a prescribed point Corollary
- 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
- Sine and cosine are 1-Lipschitz on ℝ Corollary
- The integral logarithm is continuous and strictly increasing on (0,∞) Corollary
- x sin(1/x) extended by zero is continuous but not differentiable at zero Corollary
- A curve for which the mean value inequality is an equality, showing the constant cannot be improved Counterexample
- A flat smooth real function has no holomorphic extension near zero Counterexample
- A smooth function not equal to its Maclaurin series 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 circular curve defeats the equality form of the vector-valued mean value theorem Counterexample
- The sign function is Riemann integrable on [-1,1] and has no primitive there Counterexample
- Two closed convex sets can have no strong separator 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
- x↦ x³ is a C¹ bijection whose inverse is not differentiable at zero Counterexample
- Principal inverse sine and inverse cosine Definition
- Radian angle by unit-circle arc length Definition
- The one-dimensional torus and its normalized Haar integral Definition
- Hyperbolic space is complete Example
- Normal coordinates on the round sphere Example
- The arc length of one sine period is 4√2 E(1/√2) Example
- 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
- The sine harmonics are pointwise bounded but have no uniformly convergent subsequence Example
- The solid generated by rotating y=sin x on [0,π] has volume π²/2 Example
- The surface generated by rotating y=sin x on [0,π] has area 2π(√2+arsinh1) Example
- FALSE: an invertible derivative at one point gives a local inverse False statement
- FALSE: every continuous function on a compact interval has a rectifiable graph False statement
- FALSE: every pointwise bounded sequence of continuous functions has a uniformly convergent subsequence False statement
- FALSE: if u and v are differentiable on [a,b] then ∫ₐᵇ uv' = u(b)v(b)-u(a)v(a)-∫ₐᵇ u'v False statement
- FALSE: spherical coordinates are globally injective False statement
- Finite tori are compact Hausdorff spaces separated by characters Lemma
- Higher-order Rolle theorem Lemma
- Tangent is a continuous strictly increasing bijection from (-π/2,π/2) onto ℝ Lemma
- The topologist's sine curve is connected 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
…and 28 more results.
Dependency tree · two levels
22 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
- 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)