fderivWithin_of_mem_nhdsWithin — Mathlib

English

Differentiability within insert x s at x is equivalent to differentiability within s at x.

Русский

Дифференцируемость внутри вставки x s в x эквивалентна дифференцируемости внутри s в x.

LaTeX

$$$\mathrm{DifferentiableWithinAt } 𝕜 f (\mathrm{Set.insert} x\, s) x \iff \mathrm{DifferentiableWithinAt } 𝕜 f s x$$$

Lean4

theorem fderivWithin_of_mem_nhdsWithin (st : t ∈ 𝓝[s] x) (ht : UniqueDiffWithinAt 𝕜 s x)
    (h : DifferentiableWithinAt 𝕜 f t x) : fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x :=
  ((DifferentiableWithinAt.hasFDerivWithinAt h).mono_of_mem_nhdsWithin st).fderivWithin ht

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