div — Mathlib

English

If hc and hd are HasStrictDerivAt c c' x and d has derivative d' at x with d x ≠ 0, then the division c/d has derivative given by the quotient rule with the inverse of d.

Русский

Если hc и hd задают строгую производную для c и d в x с d(x) ≠ 0, то производная c/d задается по правилу частного с обратной d.

LaTeX

$$$\\forall {hc hd hx}, HasStrictDerivAt (c/d) ((c' d x - c x d')/d x^2) x$$$

Lean4

theorem div (hc : HasStrictDerivAt c c' x) (hd : HasStrictDerivAt d d' x) (hx : d x ≠ 0) :
    HasStrictDerivAt (c / d) ((c' * d x - c x * d') / d x ^ 2) x :=
  hc.fun_div hd hx

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