fderivWithin_eq_fderiv — Mathlib

English

If s ∈ 𝓝 x, then fderivWithin 𝕜 f s x equals fderiv 𝕜 f x.

Русский

Если s принадлежит 𝓝 x, то fderivWithin 𝕜 f s x равно fderiv 𝕜 f x.

LaTeX

$$$\text{If } s \in 𝓝 x\text{ then } fderivWithin 𝕜 f s x = fderiv 𝕜 f x$$$

Lean4

theorem fderivWithin_eq_fderiv (hs : UniqueDiffWithinAt 𝕜 s x) (h : DifferentiableAt 𝕜 f x) :
    fderivWithin 𝕜 f s x = fderiv 𝕜 f x := by
  rw [← fderivWithin_univ]
  exact fderivWithin_subset (subset_univ _) hs h.differentiableWithinAt

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