fun_div — Mathlib

English

For x ≠ 0, the Fréchet derivative of the inverse function is the linear map h ↦ −h/x^2.

Русский

Для x ≠ 0 фредже-производная обратной функции — линейное отображение h ↦ −h/x^2.

LaTeX

$$$\\forall {𝕜} [NontriviallyNormedField 𝕜], x \\ne 0 \Rightarrow HasFDerivAt (\\lambda t. t^{-1}) (smulRight (1 : 𝕜 \\toL[𝕜] 𝕜) (-(x^2)^{-1})) x$$$

Lean4

theorem fun_div (hc : HasDerivWithinAt c c' s x) (hd : HasDerivWithinAt d d' s x) (hx : d x ≠ 0) :
    HasDerivWithinAt (fun y => c y / d y) ((c' * d x - c x * d') / d x ^ 2) s x :=
  by
  convert hc.fun_mul ((hasDerivAt_inv hx).comp_hasDerivWithinAt x hd) using 1
  · simp only [div_eq_mul_inv, (· ∘ ·)]
  · simp [field]
    ring

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