English
If c and d are differentiable within a set s at a point x, and d(x) ≠ 0, then the derivative within s of c/d at x is given by the quotient rule: (derivWithin c s x · d(x) − c(x) · derivWithin d s x)/d(x)^2.
Русский
Если c и d дифференцируемы внутри множества s в точке x и d(x) ≠ 0, то производная внутри s частного равна (derivWithin c s x · d(x) − c(x) · derivWithin d s x)/d(x)^2.
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 derivWithin_fun_div (hc : DifferentiableWithinAt 𝕜 c s x) (hd : DifferentiableWithinAt 𝕜 d s x) (hx : d x ≠ 0) :
derivWithin (fun x => c x / d x) s x = (derivWithin c s x * d x - c x * derivWithin d s x) / d x ^ 2 :=
by
by_cases hsx : UniqueDiffWithinAt 𝕜 s x
· exact (hc.hasDerivWithinAt.div hd.hasDerivWithinAt hx).derivWithin hsx
· simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]
