div_const — Mathlib

English

If c is differentiable on s, then the map x ↦ c(x)/d is differentiable on s.

Русский

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

LaTeX

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

Lean4

@[fun_prop]
theorem div_const (hc : DifferentiableOn 𝕜 c s) (d : 𝕜') : DifferentiableOn 𝕜 (fun x => c x / d) s := fun x hx =>
  (hc x hx).div_const d

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