differentiableWithinAt_star_iff — Mathlib

English

Differentiability of a function composed with star is equivalent to differentiability of the original function when a trivial star-structure is present.

Русский

Дифференцируемость функции после композиции со звёздочной операцией эквивалентна дифференцируемости исходной функции при тривиальной структуре звезды.

LaTeX

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

Lean4

@[simp]
theorem differentiableWithinAt_star_iff :
    DifferentiableWithinAt 𝕜 (fun y => star (f y)) s x ↔ DifferentiableWithinAt 𝕜 f s x :=
  (starL' 𝕜 : F ≃L[𝕜] F).comp_differentiableWithinAt_iff

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