differentiableWithinAt_iff — Mathlib

English

If f0 and f1 are equal near x and f0 x = f1 x, then differentiability within s at x with some derivative f' is equivalent between f0 and f1.

Русский

Если f0 и f1 совпадают в окрестности x и значения в x совпадают, тогда дифференцируемость внутри s в x с производной f' эквивалентна между f0 и f1.

LaTeX

$$$ (f_0 =_{{\\nhds[s]\,x}} f_1) \\land (f_0(x)=f_1(x)) \\Rightarrow (\\mathrm{DifferentiableWithinAt}(\\cdot) ) $$$

Lean4

theorem differentiableWithinAt_iff (h : f₀ =ᶠ[𝓝[s] x] f₁) (hx : f₀ x = f₁ x) :
    DifferentiableWithinAt 𝕜 f₀ s x ↔ DifferentiableWithinAt 𝕜 f₁ s x :=
  exists_congr fun _ => h.hasFDerivWithinAt_iff hx

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