hasDerivWithinAt — Mathlib

English

If HasDerivWithinAt f f' s x holds, then HasFDerivWithinAt f (smulRight 1 f') s x holds.

Русский

Если HasDerivWithinAt f f' s x выполняется, то HasFDerivWithinAt f (smulRight 1 f') s x также верно.

LaTeX

$$$\\text{HasDerivWithinAt}(f,f',s,x) \\Rightarrow \\text{HasFDerivWithinAt}(f,\\text{smulRight}(1,f'),s,x).$$$

Lean4

theorem hasDerivWithinAt {f' : 𝕜 →L[𝕜] F} : HasFDerivWithinAt f f' s x → HasDerivWithinAt f (f' 1) s x :=
  hasFDerivWithinAt_iff_hasDerivWithinAt.mp

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