derivWithin_div_const — Mathlib

English

For any d ≠ 0, the derivative of x ↦ c(x)/d at x equals deriv c x divided by d.

Русский

Для любого d ≠ 0 производная x ↦ c(x)/d в точке x равна производной c в x делённой на d.

LaTeX

$$$\\dfrac{d}{dx}\\left(\\dfrac{c(x)}{d}\\right) = \\dfrac{\\dfrac{d}{dx}c(x)}{d}$$$

Lean4

theorem derivWithin_div_const (hc : DifferentiableWithinAt 𝕜 c s x) (d : 𝕜') :
    derivWithin (fun x => c x / d) s x = derivWithin c s x / d := by simp [div_eq_inv_mul, derivWithin_const_mul, hc]

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