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.
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
Statement refuted
Refuted claim: if , if is continuous at a point (Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point) and if is a limit point of (Limit point, isolated point, adherent point, derived set, and dense subset of ), then is differentiable at (The derivative of at a point that is a limit point of , and differentiability on a set).
This is the converse of A function differentiable at is continuous at , and it is false. The witness is on at : a single corner is enough, and the failure is visible in one line, the difference quotient taking the value to the right of and to the left.
Facts & Assumptions
Given: The set , the function , (Basic properties of the absolute value), and the point .
Continuity of the absolute value (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): the identity is continuous at every point of its domain (claim 5), and is continuous wherever is (claim 2); so is continuous at every point of (Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point).
Derivative (The derivative of at a point that is a limit point of , and differentiability on a set): is a limit point of , punctured neighbourhoods being never empty (Limit point, isolated point, adherent point, derived set, and dense subset of , The -neighbourhood and the punctured -neighbourhood of a point of ); the difference quotient of at is on ; and is differentiable at exactly when exists (The - limit of at a limit point of ).
Absolute value (Basic properties of the absolute value): ; for ; and for .
One-sided limits (The left and right limits of at , as limits of the restrictions of to and , Intervals of : the nine order-convex forms, nondegeneracy, and length): for and , the right limit of at is the limit at of restricted to , defined when is a limit point of that set, and the left limit is the same with .
Two-sided against one-sided (If is a limit point of the domain from both sides, the limit exists iff both one-sided limits exist and agree): if is a limit point of both and , then for every real the equality holds if and only if both one-sided limits at exist and equal .
At a limit point of its domain a function has at most one limit (At a limit point of the domain a function has at most one limit); and the limit of a constant function at a limit point of its domain is , any serving (The - limit of at a limit point of ).
: (The multiplicative identity is positive) gives , and trichotomy forbids equality.
Counterexample
is continuous at every point of , in particular at .
, so the difference quotient of at is on .
and , and is a limit point of each: for every real the point lies in with , and lies in with .
For one has , so ; for one has , so . Thus restricted to is the constant and restricted to is the constant .
By [L6] and step 1.3 the two restrictions have limits at , namely and ; so by [L4] the right limit of at is and the left limit is .
Suppose for some real . By step 1.3 the point is a limit point of both one-sided sets, so [L5] forces both one-sided limits to equal ; with step 3.1 and [L6] that gives and , hence , which [L7] forbids. So has no limit at , and by [L2] the function is not differentiable at .
The refuted claim therefore fails at , and : the point is a limit point of , is continuous at by step 1.1, and is not differentiable at by step 4.1.
Remarks
-
The failure is one-sided in a precise sense. Both one-sided limits of the difference quotient exist; they simply disagree. So this is not a function whose difference quotients oscillate or blow up, and the restriction of to is differentiable at with derivative , as The derivative of at a point that is a limit point of , and differentiability on a set records when it observes that differentiability is a property of the pair (function, domain).
-
What this says about A function differentiable at is continuous at . That implication is strict: continuity is genuinely weaker than differentiability, and this witness shows the gap opens at a single point of an otherwise unremarkable function. Nothing here suggests the gap is small in any other sense; how large the set of non-differentiability of a continuous function can be is not a question this page can pose.
-
Why the argument needs If is a limit point of the domain from both sides, the limit exists iff both one-sided limits exist and agree and not merely two computations. Two different one-sided values do not by themselves contradict anything until one knows that a two-sided limit would have to agree with both, and that is exactly what the cited theorem supplies, under the hypothesis that is approached from both sides inside the domain.
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
- A function differentiable at $c$ is continuous at $c$
- The left and right limits of $f$ at $c$, as limits of the restrictions of $f$ to $A \cap (-\infty, c)$ and $A \cap (c, \infty)$
- If $c$ is a limit point of the domain from both sides, the limit exists iff both one-sided limits exist and agree
- Basic properties of the absolute value
- 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
- 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
- The $\varepsilon$-$\delta$ limit $\lim_{x \to c} f(x) = L$ of $f : A \to \mathbb{R}$ at a limit point $c$ of $A$
- Limit point, isolated point, adherent point, derived set, and dense subset of $\mathbb{R}$
- Intervals of $\mathbb{R}$: the nine order-convex forms, nondegeneracy, and length
- At a limit point of the domain a function has at most one limit
- The multiplicative identity is positive
- The $\varepsilon$-neighbourhood and the punctured $\varepsilon$-neighbourhood of a point of $\mathbb{R}$
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 55 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
- Absolute value (Wikipedia) (standard reference, not scraped)
- Differentiable function (Wikipedia) (standard reference, not scraped)
- J. Lebl, Basic Analysis I, §4.1 (standard reference, not scraped)
- T. Gantumur, Differentiation (standard reference, not scraped)