div — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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