symm_map_nhdsWithin_range — Mathlib

English

The inverse map sends nhdsWithin along the image range back to nhds on the domain: map I^{-1} (nhdsWithin (I x) (range I)) = nhds x.

Русский

Обратное отображение переводит окрестности вдоль образа обратно на исходное пространство: map I^{-1} (nhdsWithin (I x) (range I)) = nhds x.

LaTeX

$$map I^{-1} (nhdsWithin (I x) (\\operatorname{range}(I))) = nhds x$$

Lean4

theorem symm_map_nhdsWithin_range (x : H) : map I.symm (𝓝[range I] I x) = 𝓝 x := by
  rw [← I.map_nhds_eq, map_map, I.symm_comp_self, map_id]

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