differentiableWithinAt_congr_nhds

English

The differentiability within s at x is equivalent to differentiability within t at x whenever 𝓝[s] x = 𝓝[t] x.

Русский

Дифференцируемость внутри s в x эквивалентна дифференцируемости внутри t в x при равенстве 𝓝[s] x и 𝓝[t] x.

LaTeX

$$$\text{Eq }(\mathrm{nhdsWithin}(x,s), \mathrm{nhdsWithin}(x,t)) \Rightarrow (\mathrm{DifferentiableWithinAt } 𝕜 f s x \iff \mathrm{DifferentiableWithinAt } 𝕜 f t x)$$$

Lean4

theorem differentiableWithinAt_congr_nhds {t : Set E} (hst : 𝓝[s] x = 𝓝[t] x) :
    DifferentiableWithinAt 𝕜 f s x ↔ DifferentiableWithinAt 𝕜 f t x :=
  ⟨fun h => h.congr_nhds hst, fun h => h.congr_nhds hst.symm⟩

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