fun_inv — Mathlib

English

If c x ≠ 0 and HasDerivWithinAt c c' s x, then HasDerivWithinAt c^{-1} with the derivative −c'/c x^2 inside s.

Русский

Если c(x) ≠ 0 и имеет место HasDerivWithinAt c c' s x, то HasDerivWithinAt (c^{-1}) с производной −c'/c x^2 внутри s.

LaTeX

$$$\\forall {c,s,x},\\; HasDerivWithinAt c c' s x \\wedge c x \\ne 0 \\Rightarrow HasDerivWithinAt (c^{-1}) ( -c' / c x^2 ) s x$$$

Lean4

theorem fun_inv (hc : HasDerivWithinAt c c' s x) (hx : c x ≠ 0) :
    HasDerivWithinAt (fun y => (c y)⁻¹) (-c' / c x ^ 2) s x :=
  by
  convert (hasDerivAt_inv hx).comp_hasDerivWithinAt x hc using 1
  field_simp

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