derivWithin_subset — Mathlib

English

If y ∈ 𝕜 and s and t areEventually equal outside {y} near x, then derivWithin f s x = derivWithin f t x.

Русский

Если y в 𝕜 и множества s и t в окрестности x совпадают на {y}-помещении, то derivWithin f s x = derivWithin f t x.

LaTeX

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

Lean4

theorem derivWithin_subset (st : s ⊆ t) (ht : UniqueDiffWithinAt 𝕜 s x) (h : DifferentiableWithinAt 𝕜 f t x) :
    derivWithin f s x = derivWithin f t x :=
  ((DifferentiableWithinAt.hasDerivWithinAt h).mono st).derivWithin ht

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