iteratedFDerivWithin_eq_iteratedFDeriv

English

If f is C^1 at x, then f is differentiable at x.

Русский

Если функция f является C^1 в точке x, то она дифференцируема в точке x.

LaTeX

$$$ContDiffAt\ 𝕜\ 1\ f\ x\Rightarrow DifferentiableAt\ 𝕜\ f\ x$$$

Lean4

theorem iteratedFDerivWithin_eq_iteratedFDeriv {n : ℕ} (hs : UniqueDiffOn 𝕜 s) (h : ContDiffAt 𝕜 n f x) (hx : x ∈ s) :
    iteratedFDerivWithin 𝕜 n f s x = iteratedFDeriv 𝕜 n f x :=
  by
  rw [← iteratedFDerivWithin_univ]
  rcases h.contDiffOn' le_rfl (by simp) with ⟨u, u_open, xu, hu⟩
  rw [← iteratedFDerivWithin_inter_open u_open xu, ← iteratedFDerivWithin_inter_open u_open xu (s := univ)]
  apply iteratedFDerivWithin_subset
  · exact inter_subset_inter_left _ (subset_univ _)
  · exact hs.inter u_open
  · apply uniqueDiffOn_univ.inter u_open
  · simpa using hu
  · exact ⟨hx, xu⟩

Похожие утверждения