fderivWithin_congr_set' — Mathlib

English

If nhds x events equate s and t, then differentiability of f within s implies differentiability within t and vice versa.

Русский

Если окрестности x приводят к равенству множеств s и t в nhds, то дифференцируемость внутри s следует из дифференцируемости внутри t и наоборот.

LaTeX

$$$HasFDerivWithinAt f f' s x \\Rightarrow HasFDerivWithinAt f f' t x \\text{ when } s=ᶠ_{𝓝 x} t.$$$

Lean4

theorem fderivWithin_congr_set' (y : E) (h : s =ᶠ[𝓝[{ y }ᶜ] x] t) : fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x := by
  classical simp only [fderivWithin, differentiableWithinAt_congr_set' _ h, hasFDerivWithinAt_congr_set' _ h]

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