derivWithin_of_mem_nhdsWithin — Mathlib

English

If s and t coincide near x in the nhds sense, then derivWithin f s x = derivWithin f t x.

Русский

Если множества s и t совпадают в окрестности точки x в смысле nhds, то derivWithin f s x = derivWithin f t x.

LaTeX

$$$$ \\ derivWithin f s x = derivWithin f t x $$$$

Lean4

theorem derivWithin_of_mem_nhdsWithin (st : t ∈ 𝓝[s] x) (ht : UniqueDiffWithinAt 𝕜 s x)
    (h : DifferentiableWithinAt 𝕜 f t x) : derivWithin f s x = derivWithin f t x :=
  ((DifferentiableWithinAt.hasDerivWithinAt h).mono_of_mem_nhdsWithin st).derivWithin ht

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