localInverse_eventuallyEq_left — Mathlib

English

The function hf.localInverse ∘ f coincides with id on hf.localInverse.target.

Русский

Функция hf.localInverse ∘ f совпадает с тождественным отображением на hf.localInverse.target.

LaTeX

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

Lean4

theorem localInverse_eventuallyEq_left (hf : IsLocalDiffeomorphAt I J n f x) : hf.localInverse ∘ f =ᶠ[nhds x] id :=
  Filter.eventuallyEq_of_mem (hf.localInverse.open_target.mem_nhds hf.localInverse_mem_target) hf.localInverse_eqOn_left

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