right_map_implicitFunction — Mathlib

English

Near φ.pt, φ.rightFun (φ.implicitFunction p.1 p.2) equals p.2.

Русский

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

LaTeX

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

Lean4

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

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