mono_of_mem_nhdsWithin — Mathlib

English

If f is differentiable within s at x, and s ∈ 𝓝[t] x, then f is differentiable within t at x.

Русский

Если f дифференцируема внутри s в точке x и s принадлежит 𝓝[t] x, то f дифференцируема внутри t в точке x.

LaTeX

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

Lean4

theorem mono_of_mem_nhdsWithin (h : DifferentiableWithinAt 𝕜 f s x) {t : Set E} (hst : s ∈ 𝓝[t] x) :
    DifferentiableWithinAt 𝕜 f t x :=
  (h.hasFDerivWithinAt.mono_of_mem_nhdsWithin hst).differentiableWithinAt

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