map_nhdsWithin_preimage_eq — Mathlib

English

For an open embedding f and any s ⊆ β, the pushforward of the nhds within by f along x is equal to nhdsWithin at f x on the preimage s.

Русский

Для открытого вложения f и любой s ⊆ β, образ nhdsWithin по f вдоль x равен nhdsWithin в f x на предобразе s.

LaTeX

$$$\\text{IsOpenEmbedding } f \\Rightarrow \\forall s:\\ Set β,\\\\forall x:\\ α, map f (\\mathcal{N}_{f^{-1}(s)}(x)) = \\mathcal{N}_{s}(f x)$$$

Lean4

theorem map_nhdsWithin_preimage_eq {f : α → β} (hf : IsOpenEmbedding f) (s : Set β) (x : α) :
    map f (𝓝[f ⁻¹' s] x) = 𝓝[s] f x :=
  by
  rw [hf.isEmbedding.map_nhdsWithin_eq, image_preimage_eq_inter_range]
  apply nhdsWithin_eq_nhdsWithin (mem_range_self _) hf.isOpen_range
  rw [inter_assoc, inter_self]

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