map_nhds_eq — Mathlib

English

For every x, the pushforward of neighborhoods is the neighborhood within the image: map I (nhds x) = nhdsWithin (I x) (range I).

Русский

Для каждого x образ окружности переносится в окружающее множество внутри образа: map I (nhds x) = nhdsWithin (I x) (range I).

LaTeX

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

Lean4

theorem map_nhds_eq (x : H) : map I (𝓝 x) = 𝓝[range I] I x :=
  I.isClosedEmbedding.isEmbedding.map_nhds_eq x

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