map_nhdsWithin_eq — Mathlib

English

For any subset s and point x, map I of nhdsWithin x s equals nhdsWithin (I x) (I s).

Русский

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

LaTeX

$$map I (nhdsWithin x s) = nhdsWithin (I x) (\\mathrm{I}''s)$$

Lean4

theorem map_nhdsWithin_eq (s : Set H) (x : H) : map I (𝓝[s] x) = 𝓝[I '' s] I x :=
  I.isClosedEmbedding.isEmbedding.map_nhdsWithin_eq s x

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