hasDerivWithinAt_iff — Mathlib

English

Given h1: f1 =ᶠ[𝓝[s] x] f and hx: f1 x = f x, HasDerivWithinAt f1 f' s x holds if and only if HasDerivWithinAt f f' s x holds.

Русский

Пусть f1 почти эквивалентна f около x в s, и f1(x)=f(x). Тогда HasDerivWithinAt f1 f' s x эквивалентно HasDerivWithinAt f f' s x.

LaTeX

$$$HasDerivWithinAt f f' s x \\leftrightarrow HasDerivWithinAt f_1 f' s x$ при условиях $f_1 =ᶠ[𝓝[s] x] f$ и $f_1 x = f x$$$

Lean4

theorem hasDerivWithinAt_iff (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) :
    HasDerivWithinAt f₁ f' s x ↔ HasDerivWithinAt f f' s x :=
  ⟨fun h' ↦ h'.congr_of_eventuallyEq h₁.symm hx.symm, fun h' ↦ h'.congr_of_eventuallyEq h₁ hx⟩

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