prod_map_implicitFunction — Mathlib

English

Near φ.pt in the product space F × G, φ.prodFun(φ.implicitFunction(p.1, p.2)) equals p.

Русский

В окрестности точки φ.pt в произведении F × G функция φ.prodFun(неявная функция(p.1, p.2)) близка к p.

LaTeX

$$∀ᶠ p : F × G in 𝓝 (φ.prodFun φ.pt), φ.prodFun (φ.implicitFunction p.1 p.2) = p$$

Lean4

theorem prod_map_implicitFunction : ∀ᶠ p : F × G in 𝓝 (φ.prodFun φ.pt), φ.prodFun (φ.implicitFunction p.1 p.2) = p :=
  φ.hasStrictFDerivAt.eventually_right_inverse.mono fun ⟨_, _⟩ h => h

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