div_const — Mathlib

English

If c is differentiable within s at x, then c(x)/d is differentiable within s at x.

Русский

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

LaTeX

$$$DifferentiableWithinAt\$𝕜\\ c\\ s\\ x\$ \\Rightarrow DifferentiableWithinAt\\(𝕜\\ (\\lambda t. \\dfrac{c(t)}{d})\\ s\\ x$$$

Lean4

@[fun_prop]
theorem div_const (hc : DifferentiableWithinAt 𝕜 c s x) (d : 𝕜') : DifferentiableWithinAt 𝕜 (fun x => c x / d) s x :=
  (hc.hasDerivWithinAt.div_const _).differentiableWithinAt

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