fderiv_continuousLinearEquiv_comp

English

Let iso: E ≃L[𝕜] F and any f: G → E. Then DifferentiableAt 𝕜 (iso ∘ f) x is equivalent to DifferentiableAt 𝕜 f x.

Русский

Пусть iso: E ≃L[𝕜] F и любой f: G → E. Тогда DifferentiableAt 𝕜 (iso ∘ f) x эквивалентно DifferentiableAt 𝕜 f x.

LaTeX

$$$\DifferentiableAt 𝕜 (iso \circ f) x \iff \DifferentiableAt 𝕜 f x$$$

Lean4

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

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