English
Alternative form of the divisor rule within a set: the derivative within s of c/d is given by the quotient rule assuming the derivative of d is d' and d x ≠ 0.
Русский
Альтернативная форма правилa деления внутри множества: производная внутри s от c/d задается по правилу частного при допущении d x ≠ 0.
LaTeX
$$$\\forall hc hd hx, HasDerivWithinAt (c/d) s x = ((c' d x - c x d')/d x^2)$$$
Lean4
theorem fun_div (hc : HasStrictDerivAt c c' x) (hd : HasStrictDerivAt d d' x) (hx : d x ≠ 0) :
HasStrictDerivAt (fun y => c y / d y) ((c' * d x - c x * d') / d x ^ 2) x :=
by
convert hc.fun_mul ((hasStrictDerivAt_inv hx).comp x hd) using 1
· simp only [div_eq_mul_inv, (· ∘ ·)]
· simp [field]
ring
