inv₀ — Mathlib

English

If a function is C^n-differentiable within a set and nonzero, then its inverse is also C^n-differentiable within that set.

Русский

Если функция дифференцируема как C^n внутри некоторого множества и не обращается в ноль, то её обратная функция тоже C^n внутри этого множества.

LaTeX

$$ContMDiffWithinAt I' I n f s a -> f a ≠ 0 -> ContMDiffWithinAt I' I n (fun x => f x)^{-1} s a$$

Lean4

theorem inv₀ (hf : ContMDiffWithinAt I' I n f s a) (ha : f a ≠ 0) : ContMDiffWithinAt I' I n (fun x => (f x)⁻¹) s a :=
  (contMDiffAt_inv₀ ha).comp_contMDiffWithinAt a hf

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