to_local_left_inverse — Mathlib

English

If g(f x) = x eventually near a, then g has derivative f'^{-1} at f a.

Русский

Если g(f x) = x почти повсюду в окрестности a, то у g есть производная f'^{-1} в f a.

LaTeX

$$$\forall g, (\forall^{\,\} x \to x, g(f x)=x) \Rightarrow \text{HasStrictDerivAt } g f'^{-1} (f a)$$$

Lean4

theorem to_local_left_inverse {g : 𝕜 → 𝕜} (hg : ∀ᶠ x in 𝓝 a, g (f x) = x) : HasStrictDerivAt g f'⁻¹ (f a) :=
  (hf.hasStrictFDerivAt_equiv hf').to_local_left_inverse hg

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