fun_div — Mathlib

English

If c and d are differentiable functions from the base field to the target field, and d never vanishes, then the function x ↦ c(x)/d(x) is differentiable.

Русский

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

LaTeX

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

Lean4

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

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