differentiableWithinAt_congr_set'

English

If s and t are eventually equal near x, then fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x.

Русский

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

LaTeX

$$$fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x \text{ when } s=ᶠ_{𝓝 x} t.$$$

Lean4

theorem differentiableWithinAt_congr_set' (y : E) (h : s =ᶠ[𝓝[{ y }ᶜ] x] t) :
    DifferentiableWithinAt 𝕜 f s x ↔ DifferentiableWithinAt 𝕜 f t x :=
  exists_congr fun _ => hasFDerivWithinAt_congr_set' _ h

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