localInverse_right_inv — Mathlib

English

The local inverse map is itself a local diffeomorphism between the appropriate spaces.

Русский

Локальный обратный отображение само по себе является локальным диффеоморфизмом между соответствующими пространствами.

LaTeX

$$$$ \text{IsLocalDiffeomorphAt}(J,I,n, hf.localInverse, \; \text{domain}) $$$$

Lean4

theorem localInverse_right_inv (hf : IsLocalDiffeomorphAt I J n f x) {y : N} (hy : y ∈ hf.localInverse.source) :
    f (hf.localInverse y) = y :=
  by
  have : hf.localInverse y ∈ hf.choose.source :=
    by
    rw [← hf.choose.symm_target]
    exact hf.choose.symm.map_source hy
  rw [hf.choose_spec.2 this]
  exact hf.choose.right_inv hy

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