star — Mathlib

English

If a function f is differentiable on a set s, then the function y ↦ star(f(y)) is differentiable on s as well.

Русский

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

LaTeX

$$$\\text{DifferentiableOn}_{\\mathbb{K}}(f,s) \\Rightarrow \\text{DifferentiableOn}_{\\mathbb{K}}(y \\mapsto \\mathrm{star}(f(y)),s)$$$

Lean4

@[fun_prop]
protected theorem star (h : DifferentiableOn 𝕜 f s) : DifferentiableOn 𝕜 (fun y => star (f y)) s := fun x hx =>
  (h x hx).star

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