hasFDerivAtFilter_iff_hasDerivAtFilter

English

Expressing HasDerivWithinAt f f' s x in terms of HasFDerivWithinAt f f' s x with the smulRight identification.

Русский

Выражаем HasDerivWithinAt f f' s x через HasFDerivWithinAt f f' s x через соответствие smulRight.

LaTeX

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

Lean4

/-- Expressing `HasFDerivAtFilter f f' x L` in terms of `HasDerivAtFilter` -/
theorem hasFDerivAtFilter_iff_hasDerivAtFilter {f' : 𝕜 →L[𝕜] F} :
    HasFDerivAtFilter f f' x L ↔ HasDerivAtFilter f (f' 1) x L := by simp [HasDerivAtFilter]

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