congr_nhds — Mathlib

English

If nhdsWithin x s = nhdsWithin x t, then the two MDifferentiableWithinAt statements are equivalent.

Русский

Если 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 congr_nhds (h : MDifferentiableWithinAt I I' f s x) {t : Set M} (hst : 𝓝[s] x = 𝓝[t] x) :
    MDifferentiableWithinAt I I' f t x :=
  h.mono_of_mem_nhdsWithin <| hst ▸ self_mem_nhdsWithin

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