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

Exercise 10.2.6 asks to show that a function which is continuous on
[a,b], differentiable on (a,b), and has |f'| bounded by M on (a,b) is
Lipschitz with constant M on its whole domain [a,b]; the exercise
closes by defining Lipschitz continuity in those terms.  As formalized,
x and y were quantified over the open interval (a,b) instead, which
leaves out exactly the two endpoints where the Lipschitz bound is not
immediate from the mean value theorem.

The tell is that the continuity hypothesis is unused in the weaker
version: for x, y in (a,b) the segment [x,y] is contained in (a,b), so
`hderiv` alone already supplies the continuity that Corollary 10.2.9
needs, and `hcont` never enters the argument.  It is needed only to
pass to the endpoints.

Author: Chessing234

Analysis/Section_10_2.lean

@@ -106,7 +106,7 @@ theorem lipschitz_bound {M a b:ℝ} (hM: M > 0) (hab: a < b) {f:ℝ → ℝ}
   (hcont: ContinuousOn f (.Icc a b))
   (hderiv: DifferentiableOn ℝ f (.Ioo a b))
   (hlip: ∀ x ∈ Set.Ioo a b, |derivWithin f (.Ioo a b) x| ≤ M)
-  {x y:ℝ} (hx: x ∈ Set.Ioo a b) (hy: y ∈ Set.Ioo a b) :
+  {x y:ℝ} (hx: x ∈ Set.Icc a b) (hy: y ∈ Set.Icc a b) :
   |f x - f y| ≤ M * |x - y| := by
   sorry