CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-03

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.

An invertible derivative at one point does not give a local inverse without $C^{1}$ regularity

Example

Define

$f (x) : = {\begin{cases} x + 2 x^{2} \sin (1 / x), & x \neq 0, \\ 0, & x = 0. \end{cases}$

Then $f$ is differentiable at $0$ with $f^{'} (0) = 1$ , but it is injective on no neighbourhood of $0$ . Its derivative is not continuous at $0$ , so this does not contradict the $C^{1}$ inverse function theorem.

Facts & Assumptions

Given: No hypotheses beyond those quantified in the statement.

[L1]

Derivatives obey the algebra and chain rules; the power rule gives the derivatives of $x$ , $x^{2}$ , and $x^{- 1}$ on its nonzero domain; and $(\sin x)^{'} = \cos x$ (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, The derivatives of sine and cosine are cosine and minus sine).

[L2]

Sine and cosine have the integer-multiple values determined by their zero sets, periods, and quarter-turn values (The zero sets of sine and cosine and the least positive common period 2 pi, Quarter-turn values and shifts by pi/2 and pi).

[L3]

Differentiability implies continuity, and a continuous injective real function on an interval is strictly monotone (A function differentiable at $c$ is continuous at $c$ , Continuous inverse theorem: a continuous injective $f$ on an interval $I$ is a bijection onto the order-convex set $f [I]$ , and the inverse $g : f [I] \to I$ is continuous and strictly monotone in the same sense as $f$ ).

[L4]

Sine is bounded by $1$ in absolute value (Signs, monotonicity intervals, and ranges of sine and cosine).

[L5]

A derivative is the limit of the relative difference quotient (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).

Proof

technique · contradiction

1.1

At zero, $\frac{f (h) - f (0)}{h} = 1 + 2 h \sin (1 / h) ⟶ 1,$ because sine is bounded. Thus $f^{'} (0) = 1$ . For $x \neq 0$ , [L1] gives $f^{'} (x) = 1 + 4 x \sin (1 / x) - 2 \cos (1 / x) .$

L1L4L5algebra

2.1

For $n \geq 1$ , put $x_{n} : = 1 / (2 π n)$ and $y_{n} : = 1 / ((2 n + 1) π)$ . Both sequences tend to zero; [L2] gives $\sin (1 / x_{n}) = \sin (1 / y_{n}) = 0$ , $\cos (1 / x_{n}) = 1$ , and $\cos (1 / y_{n}) = - 1$ . Thus step 1.1 gives $f^{'} (x_{n}) = - 1$ and $f^{'} (y_{n}) = 3$ , so $f^{'}$ is not continuous at zero.

step 1.1L2

3.1

Suppose $f$ were injective on an open interval about zero. It is continuous there because it is differentiable, so [L3] would make it strictly increasing or strictly decreasing. At every differentiability point an increasing function has nonnegative derivative, while a decreasing function has nonpositive derivative, directly from the signs of its difference quotients. Step 2.1 supplies both a negative and a positive derivative in every such interval, a contradiction.

assume-contrastep 2.1L3L5

4.1

Thus no neighbourhood gives injectivity; step 2.1 also identifies the failure of the $C^{1}$ hypothesis.

step 2.1step 3.1L4discharge-contradiction∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

47 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

J. Lebl, Basic Analysis I, Exercise 4.4.6 (standard reference, not scraped)
J. Lebl, Basic Analysis II, Exercise 8.5.7 (standard reference, not scraped)

An invertible derivative at one point does not give a local inverse without C1C1 regularity