hasFDerivWithinAt_iff_hasDerivWithinAt

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

/-- Expressing `HasFDerivWithinAt f f' s x` in terms of `HasDerivWithinAt` -/
theorem hasFDerivWithinAt_iff_hasDerivWithinAt {f' : 𝕜 →L[𝕜] F} :
    HasFDerivWithinAt f f' s x ↔ HasDerivWithinAt f (f' 1) s x :=
  hasFDerivAtFilter_iff_hasDerivAtFilter

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