False statementConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-24

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.

FALSE: one existing iterated integral guarantees multiple Riemann integrability

Statement

False claim: if one ordinary iterated Riemann integral of a bounded function on a rectangle exists, then the function is Riemann integrable on the rectangle.

Facts & Assumptions

Given: On $[- 1, 1] \times [0, 1]$ , define $f (x, y) = x$ when $y$ is rational and $f (x, y) = 0$ when $y$ is irrational.

[F2]

A real is rational when it lies in $Q$ and irrational otherwise; both classes are dense (The Dirichlet function $1_{Q}$ , and Thomae's function $t$ with $t (x) = 1 / q$ at a rational $x = p / q$ in lowest terms with $q \geq 1$ and $t (x) = 0$ at every irrational $x$ ).

[F1]

For a Riemann-integrable function on a product rectangle, the lower and upper section-integral envelopes are integrable and have the same value; the theorem does not assert that every section of an integrable function is integrable (Riemann--Fubini on product rectangles, with lower and upper section integrals and content-zero exceptional sections).

Refutation

technique · direct

1.1

For each fixed $y$ , the $x$ -section is either $x \mapsto x$ or the zero function, and in either case its integral over $[- 1, 1]$ is $0$ . Thus the $x$ -first iterated integral exists and equals $0$ .

givenalgebra

2.1

For fixed $x \neq 0$ , density from [F2] makes the lower and upper integrals of the $y$ -section equal to $\min {x, 0}$ and $\max {x, 0}$ . Integrating these envelopes over $[- 1, 1]$ gives $- 1 / 2$ and $1 / 2$ , which are unequal; [F1] therefore rules out multiple Riemann integrability.

step 1.1F1F2algebra

3.1

The bounded function $f$ has the iterated integral from step 1.1 but is not Riemann integrable on the rectangle, so the claim is false.

step 1.1step 2.1∎

Remarks

The published One existing iterated integral does not imply multiple Riemann integrability refutes the same claim with the same witness. It lives on an examples page, so it cannot be a dependency here, and the witness is reproduced from Lebl rather than cited. A reader who has met that page has met this counterexample already.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

20 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 II, Exercise 10.2.8 (standard reference, not scraped)