fderivWithin_congr — Mathlib

English

Assume EqOn f1 f s and that f1 and f agree on s; then the derivatives within s match on nhds near x (provided f1(x)=f(x)).

Русский

Пусть f1 и f совпадают на s; тогда их касательные производные внутри s совпадают на окрестности x.

LaTeX

$$$\text{If } \mathrm{EqOn}(f_1,f,s)\text{ and } f_1(x)=f(x),\; fderivWithin 𝕜 f_1 s x = fderivWithin 𝕜 f s x.$$$

Lean4

theorem fderivWithin_congr (hs : EqOn f₁ f s) (hx : f₁ x = f x) : fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x :=
  (hs.eventuallyEq.filter_mono inf_le_right).fderivWithin_eq hx

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