hasDerivAt_exp_zero_of_radius_pos

English

For a ball around zero, exp has derivative exp(x) at x.

Русский

В шаре вокруг нуля экспонента имеет производную exp(x) в x.

LaTeX

$$$$ \HasDerivAt(\exp, \exp(x), x) $$$$

Lean4

/-- The exponential map in a complete normed field `𝕂` of characteristic zero has derivative
`1` at zero, as long as it converges on a neighborhood of zero. -/
theorem hasDerivAt_exp_zero_of_radius_pos (h : 0 < (expSeries 𝕂 𝕂).radius) : HasDerivAt (exp 𝕂) (1 : 𝕂) 0 :=
  (hasStrictDerivAt_exp_zero_of_radius_pos h).hasDerivAt

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