contDiffOn — Mathlib

English

If a function is differentiable on a set and the set is open, then it is continuously differentiable on that set.

Русский

Если функция дифференцируема на множестве и множество открыто, то она непрерывно дифференцируема на этом множестве.

LaTeX

$$ContDiffOn ℂ n f s$$

Lean4

/-- If `f : ℂ → E` is complex differentiable on some open set `s`, then it is continuously
differentiable on `s`. -/
protected theorem _root_.DifferentiableOn.contDiffOn {s : Set ℂ} {f : ℂ → E} {n : WithTop ℕ∞}
    (hd : DifferentiableOn ℂ f s) (hs : IsOpen s) : ContDiffOn ℂ n f s :=
  (hd.analyticOnNhd hs).contDiffOn_of_completeSpace

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