ThmDex – An index of mathematical definitions, results, and conjectures.
Result R2740 on D1761: Real Riemann integral
Splitting a Riemann integral over an implicit interval partition
Formulation 0
Let $[a, b] \subseteq \mathbb{R}$ be a D544: Closed real interval such that
(i) \begin{equation} a < b \end{equation}
(ii) $f : [a, b] \to \mathbb{R}$ is a D1760: Riemann integrable real function
(iii) $a = c_0, c_1, \dots, c_N = b$ is an D3687: Implicit interval partition of $[a, b]$
Then
(1) $[c_{n - 1}, c_n] \to \mathbb{R}, \quad x \mapsto f(x)$ is a D1760: Riemann integrable real function for each $n \in 1, \ldots, N$
(2) \begin{equation} \int^b_a f(x) \, d x = \sum_{n = 1}^N \int^{c_n}_{c_{n - 1}} f(x) \, d x \end{equation}
Formulation 1
Let $[a, b] \subseteq \mathbb{R}$ be a D544: Closed real interval such that
(i) \begin{equation} a < b \end{equation}
(ii) $f : [a, b] \to \mathbb{R}$ is a D1760: Riemann integrable real function
(iii) $a = c_0, c_1, \dots, c_N = b$ is an D3687: Implicit interval partition of $[a, b]$
Then
(1) $[c_{n - 1}, c_n] \to \mathbb{R}, \quad x \mapsto f(x)$ is a D1760: Riemann integrable real function for each $n \in 1, \ldots, N$
(2) \begin{equation} \int^b_a f(x) \, d x = \int^{c_N}_{c_{N - 1}} f(x) \, d x + \int^{c_{N - 1}}_{c_{N - 2}} f(x) \, d x + \cdots + \int^{c_2}_{c_1} f(x) \, d x + \int^{c_1}_{c_0} f(x) \, d x \end{equation}