fderivWithin_subset — Mathlib

English

If s ⊆ t, UniqueDiffWithinAt 𝕜 s x, and f differentiable within t at x, then fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x.

Русский

Если s ⊆ t, x уникально дифференцируем внутри s, и f дифференцируема внутри t в x, тогда fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x.

LaTeX

$$$\text{st : } s \subset t \; \land \; \mathrm{UniqueDiffWithinAt } 𝕜 s x \; \land \mathrm{DifferentiableWithinAt } 𝕜 f t x \Rightarrow fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x$$$

Lean4

theorem fderivWithin_subset (st : s ⊆ t) (ht : UniqueDiffWithinAt 𝕜 s x) (h : DifferentiableWithinAt 𝕜 f t x) :
    fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x :=
  fderivWithin_of_mem_nhdsWithin (nhdsWithin_mono _ st self_mem_nhdsWithin) ht h

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