div_const — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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