mono_of_mem_nhdsWithin — Mathlib

English

If HasFDerivWithinAt f f' t x holds and t ∈ 𝓝[s] x, then HasFDerivWithinAt f f' s x holds. In words, enlarging the neighborhood does not destroy differentiability at x when the larger set contains the smaller neighborhood of x.

Русский

Если HasFDerivWithinAt f f' t x выполнено и t ∈ 𝓝[s] x, то HasFDerivWithinAt f f' s x выполняется. Другими словами, расширение окрестности сохраняет дифференцируемость.

LaTeX

$$$$\\text{HasFDerivWithinAt } f\\,f'\\,t\\,x \\land t \\in \\mathcal{N}_s(x) \\implies \\text{HasFDerivWithinAt } f\\,f'\\,s\\,x.$$$$

Lean4

theorem mono_of_mem_nhdsWithin (h : HasFDerivWithinAt f f' t x) (hst : t ∈ 𝓝[s] x) : HasFDerivWithinAt f f' s x :=
  h.mono <| nhdsWithin_le_iff.mpr hst

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