TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-21

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 differentiable map on a connected open Euclidean set has zero derivative exactly when it is constant

Statement

Let $m, q \geq 1$ , let $U \subseteq R^{m}$ be nonempty, open, and connected, and let $f : U \to R^{q}$ be totally differentiable at every point (The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder, Vector-valued functions $f : A \to R^{m}$ , their limits and continuity, with the dictionary to the metric notions). Then $D f = 0$ on $U$ if and only if $f$ is constant on $U$ .

Facts & Assumptions

Given: The map and domain in the Statement, with polygonal paths interpreted by Polygonal paths and polygonally connected subsets of $R^{n}$ .

[L1]

Let $U \subseteq R^{n}$ be open. Then $U$ is connected if and only if it is path-connected, if and only if it is polygonally connected (For an open subset of $R^{n}$ , connectedness, path-connectedness and polygonal connectedness are equivalent).

[L2]

If $g$ is totally differentiable at $a$ and $h$ is totally differentiable at $g (a)$ , then $h \circ g$ is totally differentiable at $a$ and $D (h \circ g) (a) = D h (g (a)) \circ D g (a)$ (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

[L3]

A differentiable real function whose derivative is zero throughout an interval is constant on that interval (A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ ; consequently two such functions with the same derivative differ by a constant).

Proof

technique · direct

1.1givenalgebra

For the implication from constancy to zero derivative, a constant map has increment zero for every displacement. The zero linear map therefore leaves an identically zero remainder, so $D f (a) = 0$ at every $a \in U$ .

2.1L1L2L3given∎

For the implication from zero derivative to constancy, fix $x, y \in U$ . By [L1], a finite polygonal path in $U$ joins them. On each affine segment, [L2] makes every scalar component of the composite differentiable with derivative zero; [L3] makes that composite constant on the segment. The endpoint values agree successively along the finite path, so $f (x) = f (y)$ . Since $x, y$ were arbitrary, $f$ is constant.

A differentiable map on a connected open Euclidean set has zero derivative exactly when it is constant

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources