congr — Mathlib

English

If f1 agrees with f on s, and their derivatives match at x, then HasFDerivWithinAt f1 f' s x holds whenever HasFDerivWithinAt f f' s x holds.

Русский

Если f1 согласуется с f на s и их производные совпадают в x, то HasFDerivWithinAt f1 f' s x следует из HasFDerivWithinAt f f' s x.

LaTeX

$$$ \\mathrm{HasFDerivWithinAt}(f,f',s,x) \\to \\mathrm{EqOn}(f_1,f,s) \\to \\mathrm{Eq}(f_1(x),f(x)) \\to \\mathrm{HasFDerivWithinAt}(f_1,f',s,x) $$$

Lean4

theorem congr (h : HasFDerivWithinAt f f' s x) (hs : EqOn f₁ f s) (hx : f₁ x = f x) : HasFDerivWithinAt f₁ f' s x :=
  h.congr_mono hs hx (Subset.refl _)

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