mfderivWithin_eventually_congr_set

English

If s and t coincide eventually near x, then eventually in 𝓝 x holds mfderivWithin I I' f s y equals mfderivWithin I I' f t y.

Русский

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

LaTeX

$$$$\\forall^\\! y \\in 𝓝 x, mfderivWithin I I' f s y = mfderivWithin I I' f t y$$$$

Lean4

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

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