CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28

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 $c$ is continuous at $c$

Statement

Let $A \subseteq R$ , let $f : A \to R$ and let $c \in A$ be a limit point of $A$ (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ). If $f$ is differentiable at $c$ (The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set) then $f$ is continuous at $c$ (Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point).

Consequently, if $f$ is differentiable on a set $S \subseteq A$ then $f$ is continuous at every point of $S$ .

No converse is asserted, and none holds. Continuity at $c$ does not give differentiability at $c$ , and the standard witness is worked out on the companion page.

Facts & Assumptions

Given: A set $A \subseteq R$ , a function $f : A \to R$ and a point $c \in A$ that is a limit point of $A$ at which $f$ is differentiable (The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set, Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ).

[L1]

Carathéodory's characterisation (Carathéodory's characterisation: $f$ is differentiable at $c$ if and only if there is $φ : A \to R$ , continuous at $c$ , with $f (x) - f (c) = φ (x) (x - c)$ for every $x \in A$ , and then $φ$ is unique and $φ (c) = f^{'} (c)$ ): since $f$ is differentiable at the limit point $c$ of $A$ , there is $φ : A \to R$ , continuous at $c$ , with $f (x) - f (c) = φ (x) (x - c)$ for every $x \in A$ , and $φ (c) = f^{'} (c)$ .

[L2]

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 $A$ and the identity $x \mapsto x$ on $A$ are continuous at every point of $A$ (claim 5).

[L3]

Continuity of $f$ at $c$ is the $ε$ - $δ$ condition of Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point, and continuity on a set is continuity at each of its points.

Proof

technique · direct

1.1L1choose

Fix a function $φ : A \to R$ , continuous at $c$ , with $f (x) - f (c) = φ (x) (x - c)$ for every $x \in A$ .

1.2L2

The identity $x \mapsto x$ on $A$ and every constant function on $A$ are continuous at $c$ ; hence so is $x \mapsto x - c$ , which is the sum of the identity and the constant function with value $- c$ .

2.1step 1.1step 1.2L2

The pointwise product $x \mapsto φ (x) (x - c)$ is continuous at $c$ , being the product of two functions on $A$ continuous at $c$ .

3.1step 1.1L1

For every $x \in A$ one has $f (x) = f (c) + φ (x) (x - c)$ , so $f$ is the sum of the constant function with value $f (c)$ and the product of step 2.1.

4.1step 2.1step 3.1L2L3

A sum of two functions continuous at $c$ is continuous at $c$ , so $f$ is continuous at $c$ .

5.1step 3.1L3∎

The point $c$ was an arbitrary point of $A$ , a limit point of $A$ , at which $f$ is differentiable; applying step 4.1 at every point of a set $S \subseteq A$ on which $f$ is differentiable gives continuity of $f$ at every point of $S$ .

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 $c$ and the other tends to $0$ ; the algebra of continuous functions packages exactly that. A direct proof from the quotient would multiply and divide by $x - c$ and would have to say why that is legal, which is the same observation in a less convenient place.
The converse fails. $x \mapsto ∣ x ∣$ is continuous at $0$ and not differentiable there, which is $x \mapsto ∣ 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 ↗ 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 $f^{'}$ is defined anywhere except where it was assumed to be. Both are separate questions, and neither is settled on this page.

A function differentiable at $c$ is continuous at $c$

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

A function differentiable at cc is continuous at cc

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

A function differentiable at $c$ is continuous at $c$