Merge pull request #674 from Chessing234/ex-10-2-6-closed-interval

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

Author: teorth

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