div_const — Mathlib

English

If c has a strict derivative c' at x, then the function x ↦ c(x)/d has a strict derivative c'/d at x.

Русский

Если c имеет строгую производную c' в точке x, то x ↦ c(x)/d имеет строгую производную c'/d в x.

LaTeX

$$$HasStrictDerivAt\\left(c,c',x\\right)\\Rightarrow HasStrictDerivAt\\left(\\lambda t. \\dfrac{c(t)}{d}\\right)\\left(\\dfrac{c'}{d}\\right)\\, x$$$

Lean4

theorem div_const (hc : HasStrictDerivAt c c' x) (d : 𝕜') : HasStrictDerivAt (fun x => c x / d) (c' / d) x := by
  simpa only [div_eq_mul_inv] using hc.mul_const d⁻¹

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