div — Mathlib

English

If hc and hd are HasDerivWithinAt for c and d, d x ≠ 0, then the function y ↦ c(y)/d(y) has derivative within s given by the quotient rule with inverse of d.

Русский

Если имеют место производные внутри HasDerivWithinAt для c и d, и d(x) ≠ 0, то функция y ↦ c(y)/d(y) имеет внутри s-дериватив по правилу частного с обратной d.

LaTeX

$$$\\forall {hc hd hx},\\ HasDerivWithinAt (c/d) s x = HasDerivWithinAt (c\\cdot d^{-1}) s x = ((c' d x - c x d')/d x^2) $$$

Lean4

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

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