mdifferentiableWithinAt_congr_nhds

English

If nhdsWithin x s equals nhdsWithin x t, then equivalence between the two MDifferentiableWithinAt statements holds.

Русский

Если nhdsWithin x s = nhdsWithin x t, то равносильность между двумя утверждениями MDifferentiableWithinAt выполняется.

LaTeX

$$$ 𝓝[s] x = 𝓝[t] x \Rightarrow (MDifferentiableWithinAt I I' f s x \iff MDifferentiableWithinAt I I' f t x) $$$

Lean4

theorem mdifferentiableWithinAt_congr_nhds {t : Set M} (hst : 𝓝[s] x = 𝓝[t] x) :
    MDifferentiableWithinAt I I' f s x ↔ MDifferentiableWithinAt I I' f t x :=
  ⟨fun h => h.congr_nhds hst, fun h => h.congr_nhds hst.symm⟩

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