hasDerivAt_exp_of_mem_ball — Mathlib

English

For base field, if x lies in the ball, then HasDerivAt of exp at x equals exp(x) times 1.

Русский

Если x принадлежит ball, то имеет производную exp в x равную exp(x).

LaTeX

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

Lean4

/-- The exponential map in a complete normed field `𝕂` of characteristic zero has derivative
`NormedSpace.exp 𝕂 x` at any point `x` in the disk of convergence. -/
theorem hasDerivAt_exp_of_mem_ball [CharZero 𝕂] {x : 𝕂} (hx : x ∈ EMetric.ball (0 : 𝕂) (expSeries 𝕂 𝕂).radius) :
    HasDerivAt (exp 𝕂) (exp 𝕂 x) x :=
  (hasStrictDerivAt_exp_of_mem_ball hx).hasDerivAt

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