fix: Exercise 10.2.6 should bound |f x - f y| on the closed interval

[Chessing234]

Exercise 10.2.6 asks to show that a function which is continuous on [a,b], differentiable on (a,b), and whose derivative is bounded in absolute value by M on (a,b), satisfies |f(x) - f(y)| ≤ M|x - y| for all x, y in [a,b]. The exercise then defines Lipschitz continuity in exactly those terms, so the closed interval is the point of the statement.

The formalized version quantifies x and y over Set.Ioo a b instead, which drops precisely the two endpoints. Nothing is false as stated, but it is strictly weaker than the text, and the weakening is visible from the hypotheses: for x, y ∈ (a,b) we have [x,y] ⊆ (a,b), so hderiv alone gives Corollary 10.2.9 everything it needs and hcont is never used. Continuity on [a,b] is hypothesized precisely so that the bound extends to x or y equal to a or b, which is where the mean value theorem has to be applied on [x,y] with differentiability only on the interior.

The change is to the binders hx and hy only; the body is sorry, so no proof is affected.

I could not build locally on this machine — the Mathlib cache is not present and there is not enough free disk to fetch it — so this relies on build_book.yml in CI rather than a local lake build Analysis.Section_10_2.