mfderivWithin_congr_set — Mathlib

English

If s and t coincide eventually near x, then mfderivWithin I I' f s y equals mfderivWithin I I' f t y for all y sufficiently close to x.

Русский

Если s и t совпадают почти наверняка около x, то mfderivWithin I I' f s y равно mfderivWithin I I' f t y для всех y близких к x.

LaTeX

$$$$\\forall^\\! y \\text{ near } x,\; mfderivWithin I I' f s y = mfderivWithin I I' f t y$$$$

Lean4

/-- If two sets coincide locally, then derivatives within these sets
are the same. -/
theorem mfderivWithin_congr_set (h : s =ᶠ[𝓝 x] t) : mfderivWithin I I' f s x = mfderivWithin I I' f t x :=
  mfderivWithin_congr_set' x <| h.filter_mono inf_le_left

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