hasDerivWithinAt_iff_hasFDerivWithinAt

English

Equivalent views of HasDerivWithinAt and HasFDerivWithinAt; slope interpretation via smulRight.

Русский

Эквивалентные представления HasDerivWithinAt и HasFDerivWithinAt; касательная через smulRight.

LaTeX

$$$\\text{HasDerivWithinAt}(f,f',s,x) \\iff \\text{HasFDerivWithinAt}(f,f',s,x).$$$

Lean4

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

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