inv₀ — Mathlib

English

If a differentiable map f takes nonzero values everywhere, then its inverse is also differentiable everywhere.

Русский

Если отображение f непрерывно дифференцируемо и принимает ненулевые значения в каждой точке, то его обратное отображение также дифференцируемо в каждой точке.

LaTeX

$$ContMDiff I I n f → (∀ x, f x ≠ 0) → ContMDiff I I n (f^{-1})$$

Lean4

theorem inv₀ (hf : ContMDiffAt I' I n f a) (ha : f a ≠ 0) : ContMDiffAt I' I n (fun x ↦ (f x)⁻¹) a :=
  (contMDiffAt_inv₀ ha).comp a hf

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