star — Mathlib

English

If h : HasStrictFDerivAt f f' x, then HasStrictFDerivAt (λ x, star (f x)) (((starL' 𝕜) : F ≃L[𝕜] F) ∘L f') x.

Русский

Если функция имеет строгую фредетивную производную, то звёздочная версия функции имеет производную, получаемую как композиция со звездочным линейным отображением.

LaTeX

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

Lean4

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

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