inv

Mathlib.Analysis.Calculus.Deriv.Inv

URI: https://scilib.ai/kg/mathlib#HasDerivAt.inv

English

If HasDerivAt c c' x and c x ≠ 0, then HasDerivAt c^{-1} with derivative −c' / c x^2 at x.

Русский

Если HasDerivAt c c' x и c x ≠ 0, тогда HasDerivAt c^{-1} с производной −c' / c x^2 в точке x.

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru