hasStrictFDerivAt — Mathlib

English

From a HasFPowerSeriesWithinAt, one gets HasFDerivWithinAt with the derivative given by the first Curry-typed term evaluated at insert x s.

Русский

Из HasFPowerSeriesWithinAt следует HasFDerivWithinAt, где производная задаётся первым обработчиком цепи (Curry) в точке insert x s.

LaTeX

$$$\text{HasFDerivWithinAt}(f, \text{continuousMultilinearCurryFin1}(f))(\text{insert } x s, x)$$$

Lean4

theorem hasStrictFDerivAt (h : HasFPowerSeriesAt f p x) :
    HasStrictFDerivAt f (continuousMultilinearCurryFin1 𝕜 E F (p 1)) x := by
  simpa only [hasStrictFDerivAt_iff_isLittleO, Set.insert_eq_of_mem, Set.mem_univ, Set.univ_prod_univ,
    nhdsWithin_univ] using (h.hasFPowerSeriesWithinAt (s := Set.univ)).hasStrictFDerivWithinAt

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