hasDerivWithinAt_iff_of_mem — Mathlib

English

If h1: f1 =ᶠ[𝓝[s] x] f and hx: x ∈ s, then HasDerivWithinAt f1 f' s x is equivalent to HasDerivWithinAt f f' s x.

Русский

Если f1 совпадает с f почти около x внутри s и x ∈ s, то производная внутри s в x совпадает для f1 и f.

LaTeX

$$$(f_1 =ᶠ[𝓝[s] x] f) \\land (x \\in s) \\Rightarrow (HasDerivWithinAt f_1 f' s x \\iff HasDerivWithinAt f f' s x)$$$

Lean4

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

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