star — Mathlib

English

If HasFDerivWithinAt f f' s x, then HasFDerivWithinAt (λ x, star (f x)) (((starL' 𝕜) ∘L f')) s x.

Русский

Если HasFDerivWithinAt f f' s x, то HasFDerivWithinAt (λ x, star(f x)) (...) s x.

LaTeX

$$HasFDerivWithinAt f f' s x → HasFDerivWithinAt (fun x => star (f x)) (((starL' 𝕜).toContinuousLinearMap) ∘L f') s x$$

Lean4

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

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