fun_div — Mathlib

English

If hc and hd are differentiable at x and d x ≠ 0, then c/d is differentiable at x.

Русский

Если hc и hd дифференцируемы в x и d(x) ≠ 0, то c/d дифференцируемо в x.

LaTeX

$$$\\forall {hc hd hx}, DifferentiableAt 𝕜 (c/d) x$$$

Lean4

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

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