diff --git a/Analysis/Section_10_4.lean b/Analysis/Section_10_4.lean index fd31378c..a3ff59e0 100644 --- a/Analysis/Section_10_4.lean +++ b/Analysis/Section_10_4.lean @@ -93,7 +93,7 @@ example (q:ℚ) : (nhdsWithin 1 (.Ici 0 \ {1})).Tendsto (fun x:ℝ ↦ (x^(q:ℝ example (α:ℝ) : (nhdsWithin 1 (.Ici 0 \ {1})).Tendsto (fun x:ℝ ↦ (x^α-1^α)/(x-1)) (nhds α) := by sorry -/-- Exercise 10.4.2(b) -/ +/-- Exercise 10.4.3(b) -/ example (α:ℝ) {x:ℝ} (hx: x ∈ Set.Ici 0) : HasDerivWithinAt (fun x:ℝ ↦ x^α) (α * x^(α-1)) (.Ici 0) x := by sorry