ThmDex – An index of mathematical definitions, results, and conjectures.

Result R4730 on D1761: Real Riemann integral
Subresult of R2113: Riemann integral of a constant function

Riemann integral of a constant function on the closed unit interval

Formulation 0

Let $f : [0, 1] \to \mathbb{R}$ be a D4364: Real function such that

(i)	\begin{equation} \exists \, \lambda \in \mathbb{R} : \forall \, x \in [0, 1] : f(x) = \lambda \end{equation}

Then

(1)	$f$ is a D1760: Riemann integrable real function
(2)	\begin{equation} \int^1_0 f(x) \, d x = \lambda \end{equation}

Proofs

Proof 0

Let $f : [0, 1] \to \mathbb{R}$ be a D4364: Real function such that

(i)	\begin{equation} \exists \, \lambda \in \mathbb{R} : \forall \, x \in [0, 1] : f(x) = \lambda \end{equation}

This result is a particular case of R2113: Riemann integral of a constant function. $\square$