mdifferentiableWithinAt_congr_set

English

If s and t coincide locally around y in the specified sense, then mfderivWithin I I' f s x equals mfderivWithin I I' f t x.

Русский

Если s и t совпадают локально вокруг y в указанном смысле, то mfderivWithin I I' f s x равно mfderivWithin I I' f t x.

LaTeX

$$$$mfderivWithin I I' f s x = mfderivWithin I I' f t x$$$$

Lean4

theorem mdifferentiableWithinAt_congr_set (h : s =ᶠ[𝓝 x] t) :
    MDifferentiableWithinAt I I' f s x ↔ MDifferentiableWithinAt I I' f t x :=
  by
  simp only [mdifferentiableWithinAt_iff_exists_hasMFDerivWithinAt]
  exact exists_congr fun _ => hasMFDerivWithinAt_congr_set h

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