hasStrictFDerivAt_exp_zero — Mathlib

English

If radius positive, has StrictFDerivAt at 0 for exp.

Русский

Если радиус положителен, у экспоненты строгая ФД в 0.

LaTeX

$$$$ \HasStrictFDerivAt(\exp, 1, 0) $$$$

Lean4

/-- The exponential in a Banach algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ` has strict Fréchet derivative
`1 : 𝔸 →L[𝕂] 𝔸` at zero. -/
theorem hasStrictFDerivAt_exp_zero : HasStrictFDerivAt (exp 𝕂) (1 : 𝔸 →L[𝕂] 𝔸) 0 :=
  hasStrictFDerivAt_exp_zero_of_radius_pos (expSeries_radius_pos 𝕂 𝔸)

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