mono_of_mem_nhdsWithin — Mathlib

English

If HasDerivWithinAt f f' t x holds and t ∈ 𝓝[s] x, then HasDerivWithinAt f f' s x holds.

Русский

Если имеет место производная внутри t в точке x и t является окрестностью точки x внутри s, то имеет место производная внутри s.

LaTeX

$$$\text{HasDerivWithinAt } f\; f'\; t\; x \wedge t \in \mathcal{N}_s(x) \Rightarrow \text{HasDerivWithinAt } f\; f'\; s\; x$$$

Lean4

theorem mono_of_mem_nhdsWithin (h : HasDerivWithinAt f f' t x) (hst : t ∈ 𝓝[s] x) : HasDerivWithinAt f f' s x :=
  HasFDerivWithinAt.mono_of_mem_nhdsWithin h hst

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