map_nhdsWithin_eq — Mathlib

English

If f is an embedding, then for any s and x, the image under f of the nhdsWithin x s equals the nhdsWithin at f x of the image s.

Русский

Если f — вложение, то образ nhdsWithinx s под действием f равен nhdsWithin (f x) от образа s.

LaTeX

$$$\\text{IsEmbedding } f \\Rightarrow \\forall s\\, x:\\; \\text{map } f (\\mathcal{N}_{s}(x)) = \\mathcal{N}_{f''s}(f x)$$$

Lean4

theorem map_nhdsWithin_eq {f : α → β} (hf : IsEmbedding f) (s : Set α) (x : α) : map f (𝓝[s] x) = 𝓝[f '' s] f x :=
  hf.isInducing.map_nhdsWithin_eq s x

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