congr_nhds — Mathlib

English

If the differentiability inside s at x holds, and nhdsWithin match: 𝓝[s] x = 𝓝[t] x, then differentiability within t at x holds.

Русский

Если выполняется дифференцируемость внутри s в точке x, и 𝓝[s] x = 𝓝[t] x, то дифференцируемость внутри t в x сохраняется.

LaTeX

$$$\text{DifferentiableWithinAt } 𝕜 f s x \Rightarrow 𝓝[s] x = 𝓝[t] x \Rightarrow \text{DifferentiableWithinAt } 𝕜 f t x$$$

Lean4

theorem congr_nhds (h : DifferentiableWithinAt 𝕜 f s x) {t : Set E} (hst : 𝓝[s] x = 𝓝[t] x) :
    DifferentiableWithinAt 𝕜 f t x :=
  h.mono_of_mem_nhdsWithin <| hst ▸ self_mem_nhdsWithin

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