Measure theory 1.1.3: require boundedness in Exercise 1.1.23

[teorth]

Checked against An Introduction to Measure Theory, Exercise 1.1.23 (§1.1.3, p. 16):

Show that any continuous function f: [a,b] → R is Riemann integrable. More generally, show that any bounded, piecewise continuous function f: [a,b] → R is Riemann integrable.

(with footnote 8: "A function f: [a,b] → R is piecewise continuous if one can partition [a,b] into finitely many intervals, such that f is continuous on each interval".)

RiemannIntegrableOn.piecewise_continuous omits the boundedness hypothesis, which makes the statement false.

Counterexample. Take I = Icc 0 1, partitioned into Icc 0 0 and Ioc 0 1, and f = fun x ↦ 1/x (so f 0 = 0 by the junk-value convention). f is ContinuousOn each piece — trivially on the singleton, and 1/x is continuous on (0,1] — so hcont holds. But f is unbounded on [0,1], and unbounded functions are never Riemann integrable; the text notes this right after Definition 1.1.5, and this file already records it as RiemannIntegrable.bounded. So the sorry is unprovable as stated.

The added hypothesis uses the same idiom as RiemannIntegrable.bounded in this file, so the two compose directly. No call sites are affected — the lemma is not yet used anywhere.

Also adds the Exercise 1.1.23' docstring, which this lemma was missing (the Exercise 1.1.23 label sits on RiemannIntegrableOn.continuous just above; the text's exercise has these two sentences and no lettered parts).