fderiv_continuousLinearEquiv_comp'

English

Equivalent formulation of fderivWithin for a composition with a linear equivalence L.

Русский

Эквивалентная формулировка fderivWithin для композиции с линейным эквивалентом L.

LaTeX

$$$fderivWithin 𝕜 (Function.comp (EquivLike.toFunLike.coe iso) f) s x = (((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)) ∘L (fderivWithin 𝕜 f s x)$$$

Lean4

theorem _root_.fderiv_continuousLinearEquiv_comp' (L : G ≃L[𝕜] G') (f : E → (F →L[𝕜] G)) :
    fderiv 𝕜 (fun x ↦ (L : G →L[𝕜] G').comp (f x)) = fun x ↦
      (((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)) ∘L (fderiv 𝕜 f x) :=
  by
  ext x : 1
  exact fderiv_continuousLinearEquiv_comp L f x

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