fun_div — Mathlib

English

If c and d are differentiable on s and d x ≠ 0 for all x ∈ s, then x ↦ c(x)/d(x) is differentiable on s.

Русский

Если c и d дифференцируемы на s и для всех x ∈ s верно d(x) ≠ 0, то x ↦ c(x)/d(x) дифференцируема на s.

LaTeX

$$$\\forall x \\in s,\\ Ne(d x) = 0 \\,\\Rightarrow \\, DifferentiableOn 𝕜 (c/d) s$$$

Lean4

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

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