hasDerivWithinAt_congr_set' — Mathlib

English

If y is chosen, and the nhdsWithin complement condition holds, HasDerivWithinAt f f' s x is equivalent to HasDerivWithinAt f f' t x.

Русский

При заданном y и условии соседства, производные на s и t совпадают.

LaTeX

$$$\\text{hasDerivWithinAt_congr_set'}\\; y\\; h \\Rightarrow \\mathrm{HasDerivWithinAt}(f,f',s,x) \\iff \\mathrm{HasDerivWithinAt}(f,f',t,x).$$$

Lean4

theorem hasDerivWithinAt_congr_set' {s t : Set 𝕜} (y : 𝕜) (h : s =ᶠ[𝓝[{ y }ᶜ] x] t) :
    HasDerivWithinAt f f' s x ↔ HasDerivWithinAt f f' t x :=
  hasFDerivWithinAt_congr_set' y h

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