CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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.

Newton–Leibniz remains valid across finitely many exceptional interior points when the primitive is continuous

Statement

Let $a < b$ , let $E \subseteq [a, b]$ be finite, and let $G : [a, b] \to R$ be continuous. Suppose $G$ is differentiable at every point of $(a, b) ∖ E$ , and let $f : [a, b] \to R$ be Riemann integrable with

$f (x) = G^{'} (x) (x \in (a, b) ∖ E) .$

Then

$\int_{a}^{b} f = G (b) - G (a) .$

Points of $E$ equal to $a$ or $b$ impose no additional condition, because the hypothesis concerns only interior derivatives.

Facts & Assumptions

Given: The data in the statement.

[L1]

If a continuous function on a closed interval is differentiable in its interior and its interior derivative has an integrable extension, the extension integrates to the endpoint change (Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative).

[L2]

An integrable function restricts to closed subintervals, and its integral is additive over finitely many adjacent subintervals (For $a < c < b$ : $f$ is integrable on $[a, b]$ if and only if it is integrable on $[a, c]$ and on $[c, b]$ , and then $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; with the oriented form for arbitrary $a, b, c$ ).

Proof

technique · decomposition

1.1

List the distinct points of $E \cap (a, b)$ in increasing order as $e_{1} < \dots < e_{m}$ ; if this set is empty, take $m = 0$ . Put $e_{0} = a$ and $e_{m + 1} = b$ .

givenchoose

1.2

On every $[e_{i}, e_{i + 1}]$ , the restriction of $G$ is continuous and differentiable throughout the open subinterval, while the restriction of $f$ is integrable and agrees there with $G^{'}$ .

givenL2

2.1

Applying [L1] on each subinterval gives $\int_{e_{i}}^{e_{i + 1}} f = G (e_{i + 1}) - G (e_{i})$ .

step 1.2L1

3.1

Summing step 2.1, using [L2], and telescoping yields $\int_{a}^{b} f = G (b) - G (a)$ .

step 2.1L2

4.1

When $m = 0$ there is one subinterval and the proof is exactly [L1]; endpoint members of $E$ never occur in an open subinterval.

step 1.1step 2.1∎

Depends on

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: 47 results over 14 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

J. Lebl, Basic Analysis I & II, Exercise 5.3.3 (standard reference, not scraped)