inv — Mathlib

English

If f is ContDiffWithinAt 𝕜 n on s and f x ≠ 0 for all x ∈ s, then x ↦ (f x)^{-1} is ContDiffWithinAt 𝕜 n on s.

Русский

Если f имеет ContDiffWithinAt 𝕜 n на s и f(x) ≠ 0 для всех x∈s, то функция x↦(f(x))^{-1} имеет ContDiffWithinAt 𝕜 n на s.

LaTeX

$$$\\forall x,\\; x\\in s \\Rightarrow f(x)\\neq 0 \\Rightarrow \\mathrm{ContDiffWithinAt}_{\\mathbb{k}}\\ n\\ (x\\mapsto (f(x))^{-1})\\ s\\ x$$$

Lean4

@[fun_prop]
theorem inv {f : E → 𝕜'} {n} (hf : ContDiffWithinAt 𝕜 n f s x) (hx : f x ≠ 0) :
    ContDiffWithinAt 𝕜 n (fun x => (f x)⁻¹) s x :=
  (contDiffAt_inv 𝕜 hx).comp_contDiffWithinAt x hf

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