deriv — Mathlib

English

If f is differentiable on an open set, then the derivative on that set is differentiable again (i.e., the derivative exists and is well-behaved).

Русский

Если f дифференцируема на открытом множестве, то производная на этом множестве существует и хорошо себя ведёт.

LaTeX

$$DifferentiableOn ℂ (deriv f) s$$

Lean4

theorem _root_.DifferentiableOn.deriv {s : Set ℂ} {f : ℂ → E} (hd : DifferentiableOn ℂ f s) (hs : IsOpen s) :
    DifferentiableOn ℂ (deriv f) s :=
  (hd.analyticOnNhd hs).deriv.differentiableOn

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