hasStrictFDerivAt_equiv — Mathlib

English

Within a set s at x, the derivative of c/d is given by the expected quotient rule using derivWithin of c and d, provided d(x) ≠ 0.

Русский

Внутри множества s в точке x производная c/d задаётся обычным правилом частного, используя derivWithin c и derivWithin d, при условии d(x) ≠ 0.

LaTeX

$$$ \\operatorname{derivWithin}(c/d)\\,s\\,x = \\frac{ \\operatorname{derivWithin}(c)\\,s\\,x \\cdot d(x) - c(x) \\cdot \\operatorname{derivWithin}(d)\\,s\\,x }{ d(x)^2 } $$$

Lean4

theorem hasStrictFDerivAt_equiv {f : 𝕜 → 𝕜} {f' x : 𝕜} (hf : HasStrictDerivAt f f' x) (hf' : f' ≠ 0) :
    HasStrictFDerivAt f (ContinuousLinearEquiv.unitsEquivAut 𝕜 (Units.mk0 f' hf') : 𝕜 →L[𝕜] 𝕜) x :=
  hf

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