Аналіз I, Глава 10.1

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

API for Mathlib's HasDerivWithinAt.{u, v} {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousSMul 𝕜 F] (f : 𝕜 → F) (f' : F) (s : Set 𝕜) (x : 𝕜) : PropHasDerivWithinAt, derivWithin.{u, v} {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : 𝕜 → F) (s : Set 𝕜) (x : 𝕜) : FderivWithin, and DifferentiableWithinAt.{u_1, u_2, u_3} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : E → F) (s : Set E) (x : E) : PropDifferentiableWithinAt.

Note that the Mathlib conventions differ slightly from that in the text, in that differentiability is defined even at points that are not limit points of the domain; derivatives in such cases may not be unique, but derivWithin.{u, v} {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : 𝕜 → F) (s : Set 𝕜) (x : 𝕜) : FderivWithin still selects one such derivative in such cases (or 0 : ℕ0, if no derivative exists).

namespace Chapter10

Визначення 10.1.1 (Differentiability at a point). For the Mathlib notion HasDerivWithinAt.{u, v} {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousSMul 𝕜 F] (f : 𝕜 → F) (f' : F) (s : Set 𝕜) (x : 𝕜) : PropHasDerivWithinAt, the hypothesis that unknown identifier 'x₀'x₀ is a limit point is not needed.

theorem _root_.HasDerivWithinAt.iff (X: Set ℝ) (x₀ : ℝ) (f: ℝ → ℝ)
  (L:ℝ) :
  HasDerivWithinAt f L X x₀ ↔ Filter.Tendsto (fun x ↦ (f x - f x₀) / (x - x₀))
  (nhds x₀ ⊓ Filter.principal (X \ {x₀})) (nhds L) :=  byX:Set ℝx₀:ℝf:ℝ → ℝL:ℝ⊢ HasDerivWithinAt f L X x₀ ↔
  Filter.Tendsto (fun x => (f x - f x₀) / (x - x₀)) (nhds x₀ ⊓ Filter.principal (X \ {x₀})) (nhds L)
  rw [hasDerivWithinAt_iff_tendsto_slope, ←nhdsWithin.eq_1, iff_iff_eq, slope_fun_def_field]All goals completed! 🐙

theorem _root_.DifferentiableWithinAt.iff (X: Set ℝ) (x₀ : ℝ) (f: ℝ → ℝ) :
  DifferentiableWithinAt ℝ f X x₀ ↔ ∃ L, HasDerivWithinAt f L X x₀ := byX:Set ℝx₀:ℝf:ℝ → ℝ⊢ DifferentiableWithinAt ℝ f X x₀ ↔ ∃ L, HasDerivWithinAt f L X x₀
  constructormpX:Set ℝx₀:ℝf:ℝ → ℝ⊢ DifferentiableWithinAt ℝ f X x₀ → ∃ L, HasDerivWithinAt f L X x₀mprX:Set ℝx₀:ℝf:ℝ → ℝ⊢ (∃ L, HasDerivWithinAt f L X x₀) → DifferentiableWithinAt ℝ f X x₀
  .mpX:Set ℝx₀:ℝf:ℝ → ℝ⊢ DifferentiableWithinAt ℝ f X x₀ → ∃ L, HasDerivWithinAt f L X x₀ intro hmpX:Set ℝx₀:ℝf:ℝ → ℝh:DifferentiableWithinAt ℝ f X x₀⊢ ∃ L, HasDerivWithinAt f L X x₀
    use derivWithin f X x₀hX:Set ℝx₀:ℝf:ℝ → ℝh:DifferentiableWithinAt ℝ f X x₀⊢ HasDerivWithinAt f (derivWithin f X x₀) X x₀
    exact DifferentiableWithinAt.hasDerivWithinAt hAll goals completed! 🐙
  rintro ⟨ L, h ⟩mpr.introX:Set ℝx₀:ℝf:ℝ → ℝL:ℝh:HasDerivWithinAt f L X x₀⊢ DifferentiableWithinAt ℝ f X x₀
  exact HasDerivWithinAt.differentiableWithinAt hAll goals completed! 🐙

theorem _root_.DifferentiableWithinAt.of_hasDeriv {X: Set ℝ} {x₀ : ℝ} {f: ℝ → ℝ} {L:ℝ}
  (hL: HasDerivWithinAt f L X x₀) : DifferentiableWithinAt ℝ f X x₀ := byX:Set ℝx₀:ℝf:ℝ → ℝL:ℝhL:HasDerivWithinAt f L X x₀⊢ DifferentiableWithinAt ℝ f X x₀
  rw [DifferentiableWithinAt.iff]X:Set ℝx₀:ℝf:ℝ → ℝL:ℝhL:HasDerivWithinAt f L X x₀⊢ ∃ L, HasDerivWithinAt f L X x₀; use LAll goals completed! 🐙

theorem derivative_unique {X: Set ℝ} {x₀ : ℝ}
  (hx₀: ClusterPt x₀ (Filter.principal (X \ {x₀}))) {f: ℝ → ℝ} {L L':ℝ}
  (hL: HasDerivWithinAt f L X x₀) (hL': HasDerivWithinAt f L' X x₀) :
  L = L' := byX:Set ℝx₀:ℝhx₀:ClusterPt x₀ (Filter.principal (X \ {x₀}))f:ℝ → ℝL:ℝL':ℝhL:HasDerivWithinAt f L X x₀hL':HasDerivWithinAt f L' X x₀⊢ L = L'
    rw [_root_.HasDerivWithinAt.iff] at hL hL'X:Set ℝx₀:ℝhx₀:ClusterPt x₀ (Filter.principal (X \ {x₀}))f:ℝ → ℝL:ℝL':ℝhL:Filter.Tendsto (fun x => (f x - f x₀) / (x - x₀)) (nhds x₀ ⊓ Filter.principal (X \ {x₀})) (nhds L)hL':Filter.Tendsto (fun x => (f x - f x₀) / (x - x₀)) (nhds x₀ ⊓ Filter.principal (X \ {x₀})) (nhds L')⊢ L = L'
    rw [ClusterPt.eq_1] at hx₀X:Set ℝx₀:ℝhx₀:(nhds x₀ ⊓ Filter.principal (X \ {x₀})).NeBotf:ℝ → ℝL:ℝL':ℝhL:Filter.Tendsto (fun x => (f x - f x₀) / (x - x₀)) (nhds x₀ ⊓ Filter.principal (X \ {x₀})) (nhds L)hL':Filter.Tendsto (fun x => (f x - f x₀) / (x - x₀)) (nhds x₀ ⊓ Filter.principal (X \ {x₀})) (nhds L')⊢ L = L'
    apply tendsto_nhds_unique hL hL'All goals completed! 🐙

DifferentiableWithinAt.hasDerivWithinAt.{u, v} {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v}
  [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} (h : DifferentiableWithinAt 𝕜 f s x) :
  HasDerivWithinAt f (derivWithin f s x) s x#check DifferentiableWithinAt.hasDerivWithinAt

DifferentiableWithinAt.hasDerivWithinAt.{u, v} {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v}
  [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} (h : DifferentiableWithinAt 𝕜 f s x) :
  HasDerivWithinAt f (derivWithin f s x) s x

theorem derivative_unique' (X: Set ℝ) {x₀ : ℝ}
  (hx₀: ClusterPt x₀ (Filter.principal (X \ {x₀}))) {f: ℝ → ℝ} {L :ℝ}
  (hL: HasDerivWithinAt f L X x₀)
  (hdiff : DifferentiableWithinAt ℝ f X x₀):
  L = derivWithin f X x₀ :=
  derivative_unique hx₀ hL (DifferentiableWithinAt.hasDerivWithinAt hdiff)

Приклад 10.1.3

declaration uses 'sorry'example (x₀:ℝ) : HasDerivWithinAt (fun x ↦ x^2) (2 * x₀) (Set.univ) x₀ := byx₀:ℝ⊢ HasDerivWithinAt (fun x => x ^ 2) (2 * x₀) Set.univ x₀
  sorryAll goals completed! 🐙

declaration uses 'sorry'example (x₀:ℝ) : DifferentiableWithinAt ℝ (fun x ↦ x^2) (Set.univ) x₀ := byx₀:ℝ⊢ DifferentiableWithinAt ℝ (fun x => x ^ 2) Set.univ x₀
  sorryAll goals completed! 🐙

declaration uses 'sorry'example (x₀:ℝ) : derivWithin (fun x ↦ x^2) (Set.univ) x₀ = 2 * x₀ := byx₀:ℝ⊢ derivWithin (fun x => x ^ 2) Set.univ x₀ = 2 * x₀
  sorryAll goals completed! 🐙

Remark 10.1.4

example (X: Set ℝ) (x₀ : ℝ) {f g: ℝ → ℝ} (hfg: f = g):
  DifferentiableWithinAt ℝ f X x₀ ↔ DifferentiableWithinAt ℝ g X x₀ := byX:Set ℝx₀:ℝf:ℝ → ℝg:ℝ → ℝhfg:f = g⊢ DifferentiableWithinAt ℝ f X x₀ ↔ DifferentiableWithinAt ℝ g X x₀ rw [hfg]All goals completed! 🐙

example (X: Set ℝ) (x₀ : ℝ) {f g: ℝ → ℝ} (L:ℝ) (hfg: f = g):
  HasDerivWithinAt f L X x₀ ↔ HasDerivWithinAt g L X x₀ := byX:Set ℝx₀:ℝf:ℝ → ℝg:ℝ → ℝL:ℝhfg:f = g⊢ HasDerivWithinAt f L X x₀ ↔ HasDerivWithinAt g L X x₀ rw [hfg]All goals completed! 🐙

declaration uses 'sorry'example : ∃ (X: Set ℝ) (x₀ :ℝ) (f g: ℝ → ℝ) (L:ℝ) (hfg: f x₀ = g x₀),
  HasDerivWithinAt f L X x₀ ∧ ¬ HasDerivWithinAt g L X x₀ := by⊢ ∃ X x₀ f g L, ∃ (_ : f x₀ = g x₀), HasDerivWithinAt f L X x₀ ∧ ¬HasDerivWithinAt g L X x₀
  sorryAll goals completed! 🐙

Приклад 10.1.6

abbrev f_10_1_6 : ℝ → ℝ := abs

declaration uses 'sorry'example : Filter.Tendsto (fun x ↦ (f_10_1_6 x - f_10_1_6 0) / (x - 0))
  (nhds 0 ⊓ Filter.principal (Set.Ioi 0)) (nhds 1) := by⊢ Filter.Tendsto (fun x => (f_10_1_6 x - f_10_1_6 0) / (x - 0)) (nhds 0 ⊓ Filter.principal (Set.Ioi 0)) (nhds 1)
  sorryAll goals completed! 🐙

declaration uses 'sorry'example : Filter.Tendsto (fun x ↦ (f_10_1_6 x - f_10_1_6 0) / (x - 0))
  (nhds 0 ⊓ Filter.principal (Set.Iio 0)) (nhds (-1)) := by⊢ Filter.Tendsto (fun x => (f_10_1_6 x - f_10_1_6 0) / (x - 0)) (nhds 0 ⊓ Filter.principal (Set.Iio 0)) (nhds (-1))
  sorryAll goals completed! 🐙

declaration uses 'sorry'example : ¬ ∃ L, Filter.Tendsto (fun x ↦ (f_10_1_6 x - f_10_1_6 0) / (x - 0))
  (nhds 0 ⊓ Filter.principal (Set.univ \ {0})) (nhds L) := by⊢ ¬∃ L,
    Filter.Tendsto (fun x => (f_10_1_6 x - f_10_1_6 0) / (x - 0)) (nhds 0 ⊓ Filter.principal (Set.univ \ {0})) (nhds L) sorryAll goals completed! 🐙

declaration uses 'sorry'example : ¬ DifferentiableWithinAt ℝ f_10_1_6 (Set.univ) 0 := by⊢ ¬DifferentiableWithinAt ℝ f_10_1_6 Set.univ 0
  sorryAll goals completed! 🐙

declaration uses 'sorry'example : DifferentiableWithinAt ℝ f_10_1_6 (Set.Ioi 0) 0 := by⊢ DifferentiableWithinAt ℝ f_10_1_6 (Set.Ioi 0) 0
  sorryAll goals completed! 🐙

declaration uses 'sorry'example : derivWithin f_10_1_6 (Set.Ioi 0) 0 = 1 := by⊢ derivWithin f_10_1_6 (Set.Ioi 0) 0 = 1
  sorryAll goals completed! 🐙

declaration uses 'sorry'example : DifferentiableWithinAt ℝ f_10_1_6 (Set.Iio 0) 0 := by⊢ DifferentiableWithinAt ℝ f_10_1_6 (Set.Iio 0) 0
  sorryAll goals completed! 🐙

declaration uses 'sorry'example : derivWithin f_10_1_6 (Set.Iio 0) 0 = -1 := by⊢ derivWithin f_10_1_6 (Set.Iio 0) 0 = -1
  sorryAll goals completed! 🐙

Твердження 10.1.7 (Newton's approximation) / Вправа 10.1.2

theorem declaration uses 'sorry'_root_.HasDerivWithinAt.iff_approx_linear (X: Set ℝ) (x₀ :ℝ) (f: ℝ → ℝ) (L:ℝ) :
  HasDerivWithinAt f L X x₀ ↔
  ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀ - L * (x - x₀)| ≤ ε * |x - x₀| := byX:Set ℝx₀:ℝf:ℝ → ℝL:ℝ⊢ HasDerivWithinAt f L X x₀ ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀ - L * (x - x₀)| ≤ ε * |x - x₀|
  sorryAll goals completed! 🐙

Твердження 10.0.1 / Вправа 10.1.3

theorem declaration uses 'sorry'_root_.ContinuousWithinAt.of_differentiableWithinAt {X: Set ℝ} {x₀ : ℝ} {f: ℝ → ℝ}
  (h: DifferentiableWithinAt ℝ f X x₀) :
  ContinuousWithinAt f X x₀ := byX:Set ℝx₀:ℝf:ℝ → ℝh:DifferentiableWithinAt ℝ f X x₀⊢ ContinuousWithinAt f X x₀
  sorryAll goals completed! 🐙

/-Definition 10.1.11 (Differentiability on a domain)-/
DifferentiableOn.eq_1.{u_1, u_2, u_3} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E]
  [Module 𝕜 E] [TopologicalSpace E] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : E → F)
  (s : Set E) : DifferentiableOn 𝕜 f s = ∀ x ∈ s, DifferentiableWithinAt 𝕜 f s x#check DifferentiableOn.eq_1

DifferentiableOn.eq_1.{u_1, u_2, u_3} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E]
  [Module 𝕜 E] [TopologicalSpace E] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : E → F)
  (s : Set E) : DifferentiableOn 𝕜 f s = ∀ x ∈ s, DifferentiableWithinAt 𝕜 f s x

Наслідок 10.1.12

theorem _root_.ContinuousOn.of_differentiableOn {X: Set ℝ} {f: ℝ → ℝ}
  (h: DifferentiableOn ℝ f X) :
  ContinuousOn f X := byX:Set ℝf:ℝ → ℝh:DifferentiableOn ℝ f X⊢ ContinuousOn f X
  intro x hxX:Set ℝf:ℝ → ℝh:DifferentiableOn ℝ f Xx:ℝhx:x ∈ X⊢ ContinuousWithinAt f X x
  have hdiff := h x hxX:Set ℝf:ℝ → ℝh:DifferentiableOn ℝ f Xx:ℝhx:x ∈ Xhdiff:DifferentiableWithinAt ℝ f X x⊢ ContinuousWithinAt f X x
  exact ContinuousWithinAt.of_differentiableWithinAt hdiffAll goals completed! 🐙

Теорема 10.1.13 (a) (Differential calculus) / Вправа 10.1.4

theorem declaration uses 'sorry'_root_.HasDerivWithinAt.of_const (X: Set ℝ) (x₀ : ℝ) (c:ℝ) :
  HasDerivWithinAt (fun x ↦ c) 0 X x₀ := byX:Set ℝx₀:ℝc:ℝ⊢ HasDerivWithinAt (fun x => c) 0 X x₀ sorryAll goals completed! 🐙

Теорема 10.1.13 (b) (Differential calculus) / Вправа 10.1.4

theorem declaration uses 'sorry'_root_.HasDerivWithinAt.of_id (X: Set ℝ) (x₀ : ℝ) :
  HasDerivWithinAt (fun x ↦ x) 1 X x₀ := byX:Set ℝx₀:ℝ⊢ HasDerivWithinAt (fun x => x) 1 X x₀ sorryAll goals completed! 🐙

Теорема 10.1.13 (c) (Sum rule) / Вправа 10.1.4

theorem declaration uses 'sorry'_root_.HasDerivWithinAt.of_add {X: Set ℝ} {x₀ f'x₀ g'x₀: ℝ}
  {f g: ℝ → ℝ} (hf: HasDerivWithinAt f f'x₀ X x₀) (hg: HasDerivWithinAt g g'x₀ X x₀) :
  HasDerivWithinAt (f + g) (f'x₀ + g'x₀) X x₀ := byX:Set ℝx₀:ℝf'x₀:ℝg'x₀:ℝf:ℝ → ℝg:ℝ → ℝhf:HasDerivWithinAt f f'x₀ X x₀hg:HasDerivWithinAt g g'x₀ X x₀⊢ HasDerivWithinAt (f + g) (f'x₀ + g'x₀) X x₀
  sorryAll goals completed! 🐙

Теорема 10.1.13 (d) (Product rule) / Вправа 10.1.4

theorem declaration uses 'sorry'_root_.HasDerivWithinAt.of_mul {X: Set ℝ} {x₀ f'x₀ g'x₀: ℝ}
  {f g: ℝ → ℝ} (hf: HasDerivWithinAt f f'x₀ X x₀) (hg: HasDerivWithinAt g g'x₀ X x₀) :
  HasDerivWithinAt (f * g) (f'x₀ * (g x₀) + (f x₀) * g'x₀) X x₀ := byX:Set ℝx₀:ℝf'x₀:ℝg'x₀:ℝf:ℝ → ℝg:ℝ → ℝhf:HasDerivWithinAt f f'x₀ X x₀hg:HasDerivWithinAt g g'x₀ X x₀⊢ HasDerivWithinAt (f * g) (f'x₀ * g x₀ + f x₀ * g'x₀) X x₀
  sorryAll goals completed! 🐙

Теорема 10.1.13 (e) (Differential calculus) / Вправа 10.1.4

theorem declaration uses 'sorry'_root_.HasDerivWithinAt.of_smul {X: Set ℝ} {x₀ f'x₀: ℝ} (c:ℝ)
  {f: ℝ → ℝ} (hf: HasDerivWithinAt f f'x₀ X x₀) :
  HasDerivWithinAt (c • f) (c * f'x₀) X x₀ := byX:Set ℝx₀:ℝf'x₀:ℝc:ℝf:ℝ → ℝhf:HasDerivWithinAt f f'x₀ X x₀⊢ HasDerivWithinAt (c • f) (c * f'x₀) X x₀
  sorryAll goals completed! 🐙

Теорема 10.1.13 (f) (Difference rule) / Вправа 10.1.4

theorem declaration uses 'sorry'_root_.HasDerivWithinAt.of_sub {X: Set ℝ} {x₀ f'x₀ g'x₀: ℝ}
  {f g: ℝ → ℝ} (hf: HasDerivWithinAt f f'x₀ X x₀) (hg: HasDerivWithinAt g g'x₀ X x₀) :
  HasDerivWithinAt (f - g) (f'x₀ - g'x₀) X x₀ := byX:Set ℝx₀:ℝf'x₀:ℝg'x₀:ℝf:ℝ → ℝg:ℝ → ℝhf:HasDerivWithinAt f f'x₀ X x₀hg:HasDerivWithinAt g g'x₀ X x₀⊢ HasDerivWithinAt (f - g) (f'x₀ - g'x₀) X x₀
  sorryAll goals completed! 🐙

Теорема 10.1.13 (g) (Differential calculus) / Вправа 10.1.4

theorem declaration uses 'sorry'_root_.HasDerivWithinAt.of_inv {X: Set ℝ} {x₀ g'x₀: ℝ}
  {g: ℝ → ℝ} (hgx₀ : g x₀ ≠ 0) (hg: HasDerivWithinAt g g'x₀ X x₀) :
  HasDerivWithinAt (1/g) (-g'x₀ / (g x₀)^2) X x₀ := byX:Set ℝx₀:ℝg'x₀:ℝg:ℝ → ℝhgx₀:g x₀ ≠ 0hg:HasDerivWithinAt g g'x₀ X x₀⊢ HasDerivWithinAt (1 / g) (-g'x₀ / g x₀ ^ 2) X x₀
  sorryAll goals completed! 🐙

Теорема 10.1.13 (h) (Quotient rule) / Вправа 10.1.4

theorem declaration uses 'sorry'_root_.HasDerivWithinAt.of_div {X: Set ℝ} {x₀ f'x₀ g'x₀: ℝ}
  {f g: ℝ → ℝ} (hgx₀ : g x₀ ≠ 0) (hf: HasDerivWithinAt f f'x₀ X x₀)
  (hg: HasDerivWithinAt g g'x₀ X x₀) :
  HasDerivWithinAt (f / g) ((f'x₀ * (g x₀) - (f x₀) * g'x₀) / (g x₀)^2) X x₀ := byX:Set ℝx₀:ℝf'x₀:ℝg'x₀:ℝf:ℝ → ℝg:ℝ → ℝhgx₀:g x₀ ≠ 0hf:HasDerivWithinAt f f'x₀ X x₀hg:HasDerivWithinAt g g'x₀ X x₀⊢ HasDerivWithinAt (f / g) ((f'x₀ * g x₀ - f x₀ * g'x₀) / g x₀ ^ 2) X x₀
  sorryAll goals completed! 🐙

declaration uses 'sorry'example (x₀:ℝ) (hx₀: x₀ ≠ 1): HasDerivWithinAt (fun x ↦ (x-2)/(x-1)) (1 /(x₀-1)^2) (Set.univ \ {1}) x₀ := byx₀:ℝhx₀:x₀ ≠ 1⊢ HasDerivWithinAt (fun x => (x - 2) / (x - 1)) (1 / (x₀ - 1) ^ 2) (Set.univ \ {1}) x₀
  sorryAll goals completed! 🐙

Теорема 10.1.15 (Chain rule) / Вправа 10.1.7

theorem declaration uses 'sorry'_root_.HasDerivWithinAt.of_comp {X Y: Set ℝ} {x₀ y₀ f'x₀ g'y₀: ℝ}
  {f g: ℝ → ℝ} (hfx₀: f x₀ = y₀) (hfX : ∀ x ∈ X, f x ∈ Y)
  (hf: HasDerivWithinAt f f'x₀ X x₀) (hg: HasDerivWithinAt g g'y₀ Y y₀) :
  HasDerivWithinAt (g ∘ f) (g'y₀ * f'x₀) X x₀ := byX:Set ℝY:Set ℝx₀:ℝy₀:ℝf'x₀:ℝg'y₀:ℝf:ℝ → ℝg:ℝ → ℝhfx₀:f x₀ = y₀hfX:∀ x ∈ X, f x ∈ Yhf:HasDerivWithinAt f f'x₀ X x₀hg:HasDerivWithinAt g g'y₀ Y y₀⊢ HasDerivWithinAt (g ∘ f) (g'y₀ * f'x₀) X x₀
  sorryAll goals completed! 🐙

Вправа 10.1.5

theorem declaration uses 'sorry'_root_.HasDerivWithinAt.of_pow (n:ℕ) (x₀:ℝ) : HasDerivWithinAt (fun x ↦ x^n)
(n * x₀^((n:ℤ)-1)) (Set.univ) x₀ := byn:ℕx₀:ℝ⊢ HasDerivWithinAt (fun x => x ^ n) (↑n * x₀ ^ (↑n - 1)) Set.univ x₀
  sorryAll goals completed! 🐙

Вправа 10.1.6

theorem declaration uses 'sorry'_root_.HasDerivWithinAt.of_zpow (n:ℤ) (x₀:ℝ) (hx₀: x₀ ≠ 0) :
  HasDerivWithinAt (fun x ↦ x^n) (n * x₀^(n-1)) (Set.univ \ {0}) x₀ := byn:ℤx₀:ℝhx₀:x₀ ≠ 0⊢ HasDerivWithinAt (fun x => x ^ n) (↑n * x₀ ^ (n - 1)) (Set.univ \ {0}) x₀
  sorryAll goals completed! 🐙

end Chapter10