Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicableSession-authored (Fable 5 assisted)audited 2026-08-01
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.

The Riemann integral of a bounded function over a bounded Jordan measurable set

Definition

Let ERmE\subseteq\mathbb R^m be bounded in the metric sense of Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space and Jordan measurable, and let f:ERf:E\to\mathbb R be bounded. Choose a nondegenerate rectangle QEQ\supseteq E, whose existence follows from Jordan inner and outer content and Jordan measurable bounded sets in Rm\mathbb{R}^m, and define the zero extension f~Q(x):={f(x),xE,0,xQE.\widetilde f_Q(x):=\begin{cases}f(x),&x\in E,\\0,&x\in Q\setminus E.\end{cases} The function ff is Riemann integrable over EE when f~Q\widetilde f_Q is integrable over QQ, and then Ef:=Qf~Q.\int_Ef:=\int_Q\widetilde f_Q. Independence of the bounding rectangle, for both integrability and value, is proved in The Riemann integral over a Jordan set is independent of the bounding rectangle and recorded as the definition's forward justification. For f=1f=1, the zero extension is 1E1_E, so A bounded set is Jordan measurable iff its indicator is Riemann integrable, and the integral is its Jordan content gives E1=cont(E)\int_E1=\operatorname{cont}(E).

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 84 results over 19 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