hasFDerivAt_exp_smul_const' — Mathlib

English

Real.exp equals the NormedSpace.exp on ℝ.

Русский

Real.exp совпадает с экспонентой из NormedSpace на ℝ.

LaTeX

$$$$ \text{Real.exp} = \text{NormedSpace.exp } \mathbb{R}. $$$$

Lean4

theorem hasFDerivAt_exp_smul_const' (x : 𝔸) (t : 𝕊) :
    HasFDerivAt (fun u : 𝕊 => exp 𝕂 (u • x)) (((1 : 𝕊 →L[𝕂] 𝕊).smulRight x).smulRight (exp 𝕂 (t • x))) t :=
  hasFDerivAt_exp_smul_const_of_mem_ball' 𝕂 _ _ <| (expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _

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