div — Mathlib

English

If c and d are differentiable functions on the whole domain and d never vanishes, then the function x ↦ c(x)/d(x) is differentiable everywhere.

Русский

Если c и d дифференцируемы на всей области определения и d(x) ≠ 0 для всех x, то f(x) = c(x)/d(x) дифференцируема повсюду.

LaTeX

$$$ (\\mathrm{Differentiable}\\; c) \\rightarrow (\\mathrm{Differentiable}\\; d) \\rightarrow (\\forall x,\\; d(x) \\neq 0) \\Rightarrow \\mathrm{Differentiable}\\; (\\lambda x. c(x)/d(x)) $$$

Lean4

@[simp, fun_prop]
theorem div (hc : Differentiable 𝕜 c) (hd : Differentiable 𝕜 d) (hx : ∀ x, d x ≠ 0) : Differentiable 𝕜 (c / d) :=
  fun x => (hc x).div (hd x) (hx x)

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