fderivWithin_of_mem_nhds — Mathlib

English

If s has UniqueDiffWithinAt 𝕜 s x and f is differentiable at x, then fderivWithin 𝕜 f s x equals fderiv 𝕜 f x.

Русский

Если для множества s имеется уникальная дифференцируемость в x и f дифференцируема в x, то fderivWithin 𝕜 f s x равно fderiv 𝕜 f x.

LaTeX

$$$\text{hs : UniqueDiffWithinAt 𝕜 s x} \land \text{h : DifferentiableAt 𝕜 f x} \Rightarrow fderivWithin 𝕜 f s x = fderiv 𝕜 f x$$$

Lean4

theorem fderivWithin_of_mem_nhds (h : s ∈ 𝓝 x) : fderivWithin 𝕜 f s x = fderiv 𝕜 f x := by
  rw [← fderivWithin_univ, ← univ_inter s, fderivWithin_inter h]

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