differentiableWithinAt_iff_of_mem

English

If f0 and f1 are equal near x, and x ∈ s, then DifferentiableWithinAt for f0 within s at x with derivative f' is equivalent to DifferentiableWithinAt for f1 within s at x with derivative f'.

Русский

Если f0 и f1 совпадают около x и x∈s, то DifferentiableWithinAt внутри s в x с производной f' эквивалентно для f1.

LaTeX

$$$ (nhdsWithin x s).\\text{EventuallyEq}(f_0,f_1) \\to \\mathrm{DifferentiableWithinAt}(f_0,s,x,f') \\iff \\mathrm{DifferentiableWithinAt}(f_1,s,x,f') $$$

Lean4

theorem differentiableWithinAt_iff_of_mem (h : f₀ =ᶠ[𝓝[s] x] f₁) (hx : x ∈ s) :
    DifferentiableWithinAt 𝕜 f₀ s x ↔ DifferentiableWithinAt 𝕜 f₁ s x :=
  h.differentiableWithinAt_iff (h.eq_of_nhdsWithin hx)

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