derivWithin — Mathlib

English

If f is differentiable at x and s has a unique tangent, then derivWithin f s x equals deriv f x.

Русский

Если функция дифференцируема в точке x и множество s имеет уникальную касательную в x, то derivWithin f s x = deriv f x.

LaTeX

$$$$ \\ derivWithin f s x = deriv f x $$$$

Lean4

theorem derivWithin (h : DifferentiableAt 𝕜 f x) (hxs : UniqueDiffWithinAt 𝕜 s x) : derivWithin f s x = deriv f x :=
  by
  unfold _root_.derivWithin deriv
  rw [h.fderivWithin hxs]

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