inv — Mathlib

English

Same statement as HasDerivWithinAt.inv: if HasDerivWithinAt c c' s x and c x ≠ 0, then HasDerivWithinAt (c^{-1}) at x with derivative −c'/c x^2.

Русский

Та же формулировка, что и HasDerivWithinAt.inv: при HasDerivWithinAt c c' s x и c x ≠ 0 имеем HasDerivWithinAt (c^{-1}) с производной −c'/c x^2 в точке x.

LaTeX

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

Lean4

theorem inv (hc : HasDerivWithinAt c c' s x) (hx : c x ≠ 0) : HasDerivWithinAt (c⁻¹) (-c' / c x ^ 2) s x :=
  hc.fun_inv hx

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