hasDerivAt_iff — Mathlib

English

If h : HasDerivWithinAt f f' s x and f1 = f on s, then HasDerivWithinAt f1 f' s x.

Русский

Если у f есть производная внутри s, и f1 совпадает с f на s, то у f1 та же производная.

LaTeX

$$$HasDerivWithinAt f f' s x \\rightarrow (f_1 = f \\text{ на } s) \\rightarrow HasDerivWithinAt f_1 f' s x$$$

Lean4

theorem hasDerivAt_iff (h : f₀ =ᶠ[𝓝 x] f₁) : HasDerivAt f₀ f' x ↔ HasDerivAt f₁ f' x :=
  ⟨fun h' ↦ h'.congr_of_eventuallyEq h.symm, fun h' ↦ h'.congr_of_eventuallyEq h⟩

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