fun_div — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem fun_div (hc : DifferentiableWithinAt 𝕜 c s x) (hd : DifferentiableWithinAt 𝕜 d s x) (hx : d x ≠ 0) :
    DifferentiableWithinAt 𝕜 (fun x => c x / d x) s x :=
  (hc.hasDerivWithinAt.div hd.hasDerivWithinAt hx).differentiableWithinAt

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