congr_of_eventuallyEq — Mathlib

English

If f is differentiable within s at x and nhdsWithin x (insert x s) is used with f1 equal to f, then differentiability transfers with insertion.

Русский

Если f дифференцируема внутри s в x и используется nhdsWithin x (insert x s) с f1, равным f, то дифференцируемость переносится через вставку.

LaTeX

$$$ \\mathrm{DifferentiableWithinAt}(f,s,x) \\to \\mathrm{nhdsWithin}(x,\\mathrm{insert}\\,x\\,s)\\text{EventuallyEq}(f_1,f) \\to \\mathrm{DifferentiableWithinAt}(f_1,s,x) $$$

Lean4

theorem congr_of_eventuallyEq (h : DifferentiableWithinAt 𝕜 f s x) (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) :
    DifferentiableWithinAt 𝕜 f₁ s x :=
  (h.hasFDerivWithinAt.congr_of_eventuallyEq h₁ hx).differentiableWithinAt

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