hasStrictDerivAt_exp_zero_of_radius_pos

English

In the generalized ball, exp has strict Frechet derivative exp(x) • 1 at x.

Русский

В обобщенном шаре экспонента имеет строгую производную exp(x) • 1 в точке x.

LaTeX

$$$$ \HasStrictFDerivAt(\exp, \exp(x) \cdot 1, x) $$$$

Lean4

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

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