cderiv_eq_deriv — Mathlib

English

There exists a thickness δ>0 such that the thickening of K sits inside U and derivatives behave nicely on it.

Русский

Существуют δ>0 такие, что ct thickening(K) ⊆ U и производные сходятся равномерно на этом множестве.

LaTeX

$$$\\exists δ>0\\; (\\text{cthickening } δ K) \\subseteq U \\text{ and } TendstoUniformlyOn (deriv \\circ F) (cderiv δ f) φ K$$$

Lean4

theorem cderiv_eq_deriv [CompleteSpace E] (hU : IsOpen U) (hf : DifferentiableOn ℂ f U) (hr : 0 < r)
    (hzr : closedBall z r ⊆ U) : cderiv r f z = deriv f z :=
  two_pi_I_inv_smul_circleIntegral_sub_sq_inv_smul_of_differentiable hU hzr hf (mem_ball_self hr)

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