localInverse_eqOn_right — Mathlib

English

For any x', if x' lies in the target, applying the inverse to f(x') returns x'.

Русский

Для любого x', принадлежащего целевому множеству, применение локального обратного к f(x') возвращает x'.

LaTeX

$$$$ \text{hf.localInverse}(f(x')) = x' $$$$

Lean4

theorem localInverse_eqOn_right (hf : IsLocalDiffeomorphAt I J n f x) :
    EqOn (f ∘ hf.localInverse) id hf.localInverse.source := fun _y hy ↦ hf.localInverse_right_inv hy

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