div_const — Mathlib

English

If c is differentiable at x, then c(x)/d is differentiable at x with derivative c'/d.

Русский

Если c дифференцируема в точке x, то c(x)/d дифференцируема в x с производной c'/d.

LaTeX

$$$DifferentiableAt\$𝕜\\ c\\ x\$\\Rightarrow DifferentiableAt\$𝕜\\ (\\lambda t. \\dfrac{c(t)}{d})\\ x\$\\; \\text{with derivative }\\; \\dfrac{c'}{d}$$$

Lean4

@[simp, fun_prop]
theorem div_const (hc : DifferentiableAt 𝕜 c x) (d : 𝕜') : DifferentiableAt 𝕜 (fun x => c x / d) x :=
  (hc.hasDerivAt.div_const _).differentiableAt

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