differentiableAt_star_iff — Mathlib

English

Differentiability of f at x is equivalent to differentiability of the star-transformed function at x.

Русский

Дифференцируемость f в x эквивалентна дифференцируемости функции star(f) в x.

LaTeX

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

Lean4

@[simp]
theorem differentiableAt_star_iff : DifferentiableAt 𝕜 (fun y => star (f y)) x ↔ DifferentiableAt 𝕜 f x :=
  (starL' 𝕜 : F ≃L[𝕜] F).comp_differentiableAt_iff

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