hasDerivAt_expMap_single — Mathlib

English

The derivative of expMap_single at point x in w is given by deriv_expMap_single w x, i.e., HasDerivAt (expMap_single w) (deriv_expMap_single w x) x.

Русский

Производная экспMap_single по точке x в месте w равна deriv_expMap_single w x.

LaTeX

$$$\\mathrm{HasDerivAt}(\\mathrm{expMap\\_single}\\; w)\; (\\mathrm{deriv\\_expMap\\_single}\\; w\\; x)\\; x$$$

Lean4

theorem hasDerivAt_expMap_single (w : InfinitePlace K) (x : ℝ) :
    HasDerivAt (expMap_single w) (deriv_expMap_single w x) x := by
  simpa [expMap_single, mul_comm] using
    (HasDerivAt.comp x (Real.hasDerivAt_exp _) (hasDerivAt_mul_const (w.mult : ℝ)⁻¹))

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