implicitFunction_apply_image — Mathlib

English

For all x near φ.pt, φ.implicitFunction (φ.leftFun x) (φ.rightFun x) = x.

Русский

Для всех x близких к φ.pt функция неявной функции восстанавливает x.

LaTeX

$$∀ᶠ x in 𝓝 φ.pt, φ.implicitFunction (φ.leftFun x) (φ.rightFun x) = x$$

Lean4

theorem implicitFunction_apply_image : ∀ᶠ x in 𝓝 φ.pt, φ.implicitFunction (φ.leftFun x) (φ.rightFun x) = x :=
  φ.hasStrictFDerivAt.eventually_left_inverse

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