star — Mathlib

English

If f is differentiable at x, then the function y ↦ star(f(y)) is differentiable at x as well.

Русский

Если f дифференцируема в x, то функция y ↦ star(f(y)) также дифференциируется в x.

LaTeX

$$$DifferentiableAt\ 𝕜\ f x \Rightarrow DifferentiableAt\ 𝕜\ (\lambda y, star (f y)) x$$$

Lean4

@[fun_prop]
protected theorem star (h : DifferentiableAt 𝕜 f x) : DifferentiableAt 𝕜 (fun y => star (f y)) x :=
  h.hasFDerivAt.star.differentiableAt

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