mfderivWithin_eventually_congr_set'

English

If s and t coincide near x, then mfderivWithin I I' f s x equals mfderivWithin I I' f t x.

Русский

Если s и t совпадают поблизости от x, то 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

/-- If two sets coincide locally, except maybe at a point, then derivatives within these sets
coincide locally. -/
theorem mfderivWithin_eventually_congr_set' (y : M) (h : s =ᶠ[𝓝[{ y }ᶜ] x] t) :
    ∀ᶠ y in 𝓝 x, mfderivWithin I I' f s y = mfderivWithin I I' f t y :=
  (eventually_nhds_nhdsWithin.2 h).mono fun _ => mfderivWithin_congr_set' y

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