map_nhdsWithin_eq — Mathlib

English

If f and g satisfy a left-inverse relation on s, then map g preserves nhds within s.

Русский

Если f и g удовлетворяют отношению левого обратного на s, отображение g сохраняет окрестности nhds внутри s.

LaTeX

$$$\\text{LeftInvOn } f\\ g\\ s \\Rightarrow \\text{map } g (\\mathcal{N}_{s}) = \\mathcal{N}_{g''s}$$$

Lean4

theorem map_nhdsWithin_eq {f : α → β} (hf : IsInducing f) (s : Set α) (x : α) : map f (𝓝[s] x) = 𝓝[f '' s] f x := by
  ext; simp +contextual [mem_nhdsWithin_iff_eventually, hf.nhds_eq_comap, forall_comm (α := _ ∈ _)]

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