localInverse_eventuallyEq_right — Mathlib

English

The composition hf.localInverse ∘ f equals id on the domain hf.localInverse.source.

Русский

Состав hf.localInverse ∘ f совпадает с тождественным отображением на области определения hf.localInverse.

LaTeX

$$$$ (hf.localInverse \circ f) = \mathrm{id} \text{ on } hf.localInverse.source. $$$$

Lean4

theorem localInverse_eventuallyEq_right (hf : IsLocalDiffeomorphAt I J n f x) : f ∘ hf.localInverse =ᶠ[nhds (f x)] id :=
  Filter.eventuallyEq_of_mem (hf.localInverse.open_source.mem_nhds hf.localInverse_mem_source)
    hf.localInverse_eqOn_right

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