localInverse_left_inv — Mathlib

English

The inverse composed with f is equal to id on the intersection of the domain with the inverse's target.

Русский

Обратное, применённое к f, совпадает с тождественным отображением на пересечении области определения и целевого множества обратного.

LaTeX

$$$$ (hf.localInverse \circ f) =_{hf.localInverse.target} \mathrm{id}. $$$$

Lean4

theorem localInverse_left_inv (hf : IsLocalDiffeomorphAt I J n f x) {x' : M} (hx' : x' ∈ hf.localInverse.target) :
    hf.localInverse (f x') = x' :=
  by
  rw [hf.choose_spec.2 (hf.choose.symm_target ▸ hx')]
  exact hf.choose.left_inv hx'

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