Alphabeta MathHow 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.
Tagged grid partitions and Riemann sums in
Definition
A tagging of a grid assigns to every cell a point . The lower corner is a canonical tagging, so taggings exist without choice. The Riemann sum is with the iterated sum convention of Grid partitions of a rectangle in , their cells, refinements and mesh.
The tagged sums converge with mesh to if for every some makes for every tagged grid with mesh below . Finite cellwise selections used in proofs are licensed by Every natural-number-indexed list of nonempty sets has a choice function on its family of values and Choice function, not by countable choice.
For bounded , each tag lies in its cell, so termwise inequalities and nonnegative volumes give (Lower and upper Darboux sums over a grid partition in , Lower bound, bounded below, bounded set).
Depends on
- Grid partitions of a rectangle in $\mathbb{R}^m$, their cells, refinements and mesh
- Lower and upper Darboux sums over a grid partition in $\mathbb{R}^m$
- Axis-parallel rectangles in $\mathbb{R}^m$ and their volume
- Every natural-number-indexed list of nonempty sets has a choice function on its family of values
- Choice function
- Lower bound, bounded below, bounded set
Used by
Dependency tree · two levels
29 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, Riemann Integral in Several Variables (standard reference, not scraped)
- J. Lebl, Basic Analysis, The Riemann-Lebesgue Criterion (standard reference, not scraped)