inv — Mathlib

English

In a setting with HasSummableGeomSeries, the map x ↦ (x)^{-1} is ContDiffAt 𝕜 n at invertible x.

Русский

При условии HasSummableGeomSeries отображение x↦x^{-1} является ContDiffAt 𝕜 n в обратимой x.

LaTeX

$$$[HasSummableGeomSeries R]\\; (x: R^{\\times})\\; \\mathrm{ContDiffAt}_{\\mathbb{k}}\\ n\\ \\mathrm{Ring.inverse}\\ x$$$

Lean4

@[fun_prop]
theorem inv {f : E → 𝕜'} (hf : ContDiff 𝕜 n f) (h : ∀ x, f x ≠ 0) : ContDiff 𝕜 n fun x => (f x)⁻¹ := by
  rw [contDiff_iff_contDiffAt];
  exact fun x =>
    hf.contDiffAt.inv
      (h x)
        -- TODO: generalize to `f g : E → 𝕜'`

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