star — Mathlib

English

In derivWithin, the derivative of star(f) equals star of derivative of f, under mild conditions.

Русский

В производной внутри существует равенство: derivative of star(f) = star of derivative of f.

LaTeX

$$protected theorem star : derivWithin (fun y => star (f y)) s x = star (derivWithin f s x)$$

Lean4

protected theorem star : derivWithin (fun y => star (f y)) s x = star (derivWithin f s x) :=
  by
  by_cases hxs : UniqueDiffWithinAt 𝕜 s x
  · exact DFunLike.congr_fun (fderivWithin_star hxs) _
  · simp [derivWithin_zero_of_not_uniqueDiffWithinAt hxs]

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