contDiffOn_zero — Mathlib

English

If ContDiffOn 𝕜 1 f s, then f is differentiable on s.

Русский

Если ContDiffOn 𝕜 1 f s, то f дифференцируема на s.

LaTeX

$$$ContDiffOn\\ 𝕜\\ 1\\ f\\ s\\rightarrow DifferentiableOn\\ 𝕜\\ f\\ s$$$

Lean4

@[simp]
theorem contDiffOn_zero : ContDiffOn 𝕜 0 f s ↔ ContinuousOn f s :=
  by
  refine ⟨fun H => H.continuousOn, fun H => fun x hx m hm ↦ ?_⟩
  have : (m : WithTop ℕ∞) = 0 := le_antisymm (mod_cast hm) bot_le
  rw [this]
  refine ⟨insert x s, self_mem_nhdsWithin, ftaylorSeriesWithin 𝕜 f s, ?_⟩
  rw [hasFTaylorSeriesUpToOn_zero_iff]
  exact ⟨by rwa [insert_eq_of_mem hx], fun x _ => by simp [ftaylorSeriesWithin]⟩

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