fun_inv — Mathlib

English

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

Русский

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

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 fun_inv (hc : HasDerivAt c c' x) (hx : c x ≠ 0) : HasDerivAt (fun y => (c y)⁻¹) (-c' / c x ^ 2) x :=
  by
  rw [← hasDerivWithinAt_univ] at *
  exact hc.inv hx

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