hasFDerivAt_expMapBasis — Mathlib

English

The derivative of expMapBasis at x equals the composition of fderiv_expMapBasis x with the inverse of the linear isomorphism (completeBasis K).equivFunL.

Русский

Производная функций expMapBasis в точке x равна композиции fderiv_expMapBasis x с обратным линейным изоморфизмом (completeBasis K).equivFunL.

LaTeX

$$$\text{HasFDerivAt }(\expMapBasis)(\,\text{fderiv\_expMapBasis } K\, x)(x)$$$

Lean4

theorem hasFDerivAt_expMapBasis (x : realSpace K) : HasFDerivAt expMapBasis (fderiv_expMapBasis K x) x :=
  by
  change HasFDerivAt (expMap ∘ (completeBasis K).equivFunL.symm) (fderiv_expMapBasis K x) x
  exact (hasFDerivAt_expMap _).comp x (completeBasis K).equivFunL.symm.hasFDerivAt

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