theorem continuousOn_riemannIntegrableOn {a b : ℝ} {f : ℝ → ℝ} (hcont : ContinuousOn f (Set.Icc a b)) : RiemannIntegrableOn f a b

Lemma 5.2.7: A continuous function on a closed bounded interval [a, b] belongs to ℛ([a, b]), i.e., it is Riemann integrable on that interval.

theorem riemannIntegral_tendsto_of_nested_intervals {a b : ℝ} {f : ℝ → ℝ} (hbound : ∃ (M : ℝ), ∀ x ∈ Set.Icc a b, |f x| ≤ M) {a_seq b_seq : ℕ → ℝ} (h_between : ∀ (n : ℕ), a < a_seq n ∧ a_seq n < b_seq n ∧ b_seq n < b) (ha : Filter.Tendsto a_seq Filter.atTop (nhds a)) (hb : Filter.Tendsto b_seq Filter.atTop (nhds b)) (hf_seq : ∀ (n : ℕ), RiemannIntegrableOn f (a_seq n) (b_seq n)) : ∃ (hf_ab : RiemannIntegrableOn f a b), Filter.Tendsto (fun (n : ℕ) => riemannIntegral f (a_seq n) (b_seq n) ⋯) Filter.atTop (nhds (riemannIntegral f a b hf_ab))

Lemma 5.2.8: Let f : [a, b] → ℝ be bounded, and suppose sequences aₙ, bₙ satisfy a < aₙ < bₙ < b for all n with aₙ → a and bₙ → b. If f ∈ ℛ([aₙ, bₙ]) for every n, then f ∈ ℛ([a, b]) and ∫_a^b f = lim_{n → ∞} ∫_{aₙ}^{bₙ} f.

theorem continuousOn_Icc_of_continuousAt {a b : ℝ} {f : ℝ → ℝ} (hcont : ∀ x ∈ Set.Icc a b, ContinuousAt f x) : ContinuousOn f (Set.Icc a b)

theorem riemannIntegrableOn_of_continuousAt_Ioo {a b : ℝ} {f : ℝ → ℝ} (hbound : ∃ (M : ℝ), ∀ x ∈ Set.Icc a b, |f x| ≤ M) (hcont : ∀ x ∈ Set.Ioo a b, ContinuousAt f x) : RiemannIntegrableOn f a b

theorem riemannIntegrableOn_of_finite_discontinuities {a b : ℝ} {f : ℝ → ℝ} (hbound : ∃ (M : ℝ), ∀ x ∈ Set.Icc a b, |f x| ≤ M) (hfinite : {x : ℝ | x ∈ Set.Icc a b ∧ ¬ContinuousAt f x}.Finite) : RiemannIntegrableOn f a b

Theorem 5.2.9: A bounded function on [a, b] with only finitely many discontinuities belongs to ℛ([a, b]), i.e., it is Riemann integrable.

theorem riemannIntegral_congr_on_Icc {a b : ℝ} {f g : ℝ → ℝ} (hfg : ∀ x ∈ Set.Icc a b, g x = f x) (hf : RiemannIntegrableOn f a b) : ∃ (hg : RiemannIntegrableOn g a b), riemannIntegral g a b hg = riemannIntegral f a b hf

If two functions agree on Set.Icc a b, they are simultaneously Riemann integrable and have the same integral.