inv — Mathlib

English

If hf is ContDiffAt 𝕜 n f x and f x ≠ 0, then the map x ↦ (f x)^{-1} is ContDiffAt 𝕜 n at x.

Русский

Если f является ContDiffAt 𝕜 n в x и f(x) ≠ 0, то x↦(f(x))^{-1} — ContDiffAt 𝕜 n в x.

LaTeX

$$$\\mathrm{ContDiffAt}_{\\mathbb{k}}\\ n\\ f\\ x \\to\\mathrm{ContDiffAt}_{\\mathbb{k}}\\ n\\ (x\\mapsto (f(x))^{-1})\\ x$$$

Lean4

@[fun_prop]
theorem inv {f : E → 𝕜'} (hf : ContDiffOn 𝕜 n f s) (h : ∀ x ∈ s, f x ≠ 0) : ContDiffOn 𝕜 n (fun x => (f x)⁻¹) s :=
  fun x hx => (hf.contDiffWithinAt hx).inv (h x hx)

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