ThmDex – An index of mathematical definitions, results, and conjectures.
 ▼ Set of symbols ▼ Alphabet ▼ Deduction system ▼ Theory ▼ Zermelo-Fraenkel set theory ▼ Set ▼ Binary cartesian set product ▼ Binary relation ▼ Binary endorelation ▼ Preordering relation ▼ Partial ordering relation ▼ Partially ordered set ▼ Closed interval ▼ Implicit interval partition ▼ Implicit basic real interval partition ▼ Closed real interval tagged partition ▼ Stieltjes sum ▼ Riemann sum
Definition D1760
Riemann integrable real function

Let $[a, b] \subset \mathbb{R}$ be a D544: Closed real interval such that
 (i) $$a < b$$ (ii) $f : [a, b] \to \mathbb{R}$ is a D4364: Real function on $[a, b]$
Then $f$ is a Riemann integrable real function on $[a, b]$ if and only if $$\exists \, R \in \mathbb{R} : \forall \, \varepsilon > 0 : \exists \, \delta > 0 \left( P \text{ is a tagged partition for } [a, b] \text{ with } \text{Mesh}(P) < \delta \quad \implies \quad \left| \mathcal{R}_P(f) - R \right| < \varepsilon \right)$$