star — Mathlib

English

If f has a strict Fréchet derivative f' at x, then the map z ↦ star(f(z)) has derivative given by starL' ∘ f'.

Русский

Если у f в точке x есть строгая фреше производная f', то отображение z ↦ звезда(f(z)) имеет производную, равную starL' ∘ f'.

LaTeX

$$HasStrictFDerivAt f f' x → HasStrictFDerivAt (fun z => star (f z)) (((starL' 𝕜) : F ≃L[𝕜] F) ∘L f') x$$

Lean4

@[fun_prop]
protected theorem star (h : HasStrictFDerivAt f f' x) :
    HasStrictFDerivAt (fun x => star (f x)) (((starL' 𝕜 : F ≃L[𝕜] F) : F →L[𝕜] F) ∘L f') x :=
  (starL' 𝕜 : F ≃L[𝕜] F).toContinuousLinearMap.hasStrictFDerivAt.comp x h

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