mfderivWithin_subset — Mathlib

English

If h is MDifferentiableWithinAt on s and s ∈ 𝓝[t] x, then h is MDifferentiableWithinAt on t.

Русский

Если h выполняется внутри s и s принадлежит 𝓝[t] x, то h выполняется внутри t.

LaTeX

$$$ (h : MDifferentiableWithinAt I I' f s x) {t : Set M} (hst : s ∈ 𝓝[t] x) : MDifferentiableWithinAt I I' f t x $$$

Lean4

theorem mfderivWithin_subset (st : s ⊆ t) (hs : UniqueMDiffWithinAt I s x) (h : MDifferentiableWithinAt I I' f t x) :
    mfderivWithin I I' f s x = mfderivWithin I I' f t x :=
  ((MDifferentiableWithinAt.hasMFDerivWithinAt h).mono st).mfderivWithin hs

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