left_map_implicitFunction — Mathlib

English

Near φ.pt in the product space, φ.leftFun (φ.implicitFunction p.1 p.2) equals p.1.

Русский

В окрестности точки φ.pt левая компонента осуществления неявной функции равна первой компоненте p.

LaTeX

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

Lean4

theorem left_map_implicitFunction : ∀ᶠ p : F × G in 𝓝 (φ.prodFun φ.pt), φ.leftFun (φ.implicitFunction p.1 p.2) = p.1 :=
  φ.prod_map_implicitFunction.mono fun _ => congr_arg Prod.fst

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