differentiableOn_star_iff — Mathlib

English

DifferentiableOn 𝕜 (fun y => star (f y)) s if and only if DifferentiableOn 𝕜 f s.

Русский

Дифференцируемость 𝕜 функции f на s эквивалентна дифференцируемости её образа под star на s.

LaTeX

$$$\\text{DifferentiableOn}_{\\mathbb{K}}(\\lambda y. \\mathrm{star}(f(y)),s) \\iff \\text{DifferentiableOn}_{\\mathbb{K}}(f,s)$$$

Lean4

@[simp]
theorem differentiableOn_star_iff : DifferentiableOn 𝕜 (fun y => star (f y)) s ↔ DifferentiableOn 𝕜 f s :=
  (starL' 𝕜 : F ≃L[𝕜] F).comp_differentiableOn_iff

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