mfderivWithin_of_mem_nhds — Mathlib

English

If nhdsWithin x s equals nhdsWithin x t, then equivalence of the MDifferentiableWithinAt statements holds.

Русский

Если nhdsWithin x s = nhdsWithin x t, то эквивалентность утверждений MDifferentiableWithinAt сохраняется.

LaTeX

$$$ 𝓝[s] x = 𝓝[t] x \Rightarrow (MDifferentiableWithinAt I I' f s x \iff MDifferentiableWithinAt I I' f t x) $$$

Lean4

theorem mfderivWithin_of_mem_nhds (h : s ∈ 𝓝 x) : mfderivWithin I I' f s x = mfderiv I I' f x := by
  rw [← mfderivWithin_univ, ← univ_inter s, mfderivWithin_inter h]

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