mdifferentiableWithinAt_iff_exists_hasMFDerivWithinAt

English

If MDifferentiableWithinAt holds on s and s is nhdsWithin-subset of t, then it holds on t.

Русский

Если MDifferentiableWithinAt верно на s и s ⊆_nhds t, то верно на t.

LaTeX

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

Lean4

theorem mdifferentiableWithinAt_iff_exists_hasMFDerivWithinAt :
    MDifferentiableWithinAt I I' f s x ↔ ∃ f', HasMFDerivWithinAt I I' f s x f' :=
  by
  refine ⟨fun h ↦ ⟨mfderivWithin I I' f s x, h.hasMFDerivWithinAt⟩, ?_⟩
  rintro ⟨f', hf'⟩
  exact hf'.mdifferentiableWithinAt

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